How to translate set propositions involving power sets and cartesian products, into first-order logic statements? As seen from an earlier question of mine one can translate between set algebra and logic, as long as they speak about elements (a named set A is the same as {x ∣ x ∈ A}).
However I've stumbled upon propositions that involve cartesian products and power sets and I'm not sure how to translate those into logic statements. For instance:
(A  × B)    =   (B  × A)    if and only if  A   =   B
or


*

*if   A   =   ℘(A)    then    ℘(A)    =   ∅

*if   A   ⊆ ℘(A)  then    ℘(A)    =   ∅

*if A ∈ ℘(A)  then    ℘(A)    =   ∅


and even a combination of the two:
℘(A ×   B)  ⊆       ℘(A)    ×   ℘(B)
Note that "×" is the cartesian product symbol, and ℘ the power-set.
Can someone provide any insight on this?
 A: Most introductory books on axiomatic set theory directly define set theoretical concepts in the language of first order logic. Once you know these definitions, all you need to do is translate, translate and translate until you are satisfied. One such book that I use can be found here: http://www.amazon.com/Theory-Continuum-Problem-Dover-Mathematics/dp/0486474844. If you buy this book, I warn you that it has errors. Fortunately, you can find a lot of the corrections here: http://comet.lehman.cuny.edu/fitting/errata/book_errors/RevisedSetBookErrors/split.html.
I also noticed that in the answer to your earlier question, set builder notation $\{x:\Phi(x)\}$ was used a lot. While this is not necessarily wrong, it can lead you dangerously close to Bertrand Russell's paradox. Briefly, just let $\Phi(x)$ be $x \not\in x$. Then, the entity $X = \{x:x \not\in x\}$ cannot itself be a set in the sense that it can never sit on the left hand side of the symbol $\in$ (i.e. $X \in \mathcal{S}$ is invalid syntax for any symbol $\mathcal{S}$). If it could, then either $X \in X$ or $X \not\in X$. Either case leads to a contradiction.
Thus, I will show you an alternate way of encoding set theory in first order logic. To start with, the book I referred to above studies a popular axiomatization of set theory: Von Neumann–Bernays–Gödel (NBG) set theory. This theory talks not only about sets but also about classes. The intuition behind a class is that it is an arbitrary collection of things. A set is a class that is contained in some other class. Thus, sets are just "smaller" collections of things. Now, to show you how NBG encodes set theory in first order logic, we need to be a bit more precise with our language.
I reserve the CAPITAL letters $A, B, C, ..., X, Y, Z$ with or without sub(super)scripts to denote classes. I reserve the small letters $a, b, c, ..., x, y, z$ with or without sub(super)scripts to denote sets. Appearance aside, the capital and small letters also have different usage. How so? Well, we first introduce a binary symbol $\in$. Then we impose the following condition on it: only small letters can sit on the left of this symbol while both small and capital letters can sit on its right. Hence $x \in A$ is valid while $B \in A$ is not. Thus, we have implicitly said that only sets (small letters) can be elements.
With these preliminaries, we can start defining things. I skip many technicalities to keep the exposition brief. For instance, I do not mention any axioms of set theory itself. I can come back to them later on if you want me to. For now:


*

*We introduce a binary symbol $\subseteq$ which is used in the following way: $A \subseteq B$ is short for $\forall x(x \in A \to x \in B)$ or if you prefer to be more formal: $A \subseteq B \leftrightarrow \forall x(x \in A \to x\in B)$.

*Similarly, we introduce a binary symbol $=$: $A = B$ is short for $A \subseteq B \wedge B \subseteq A$.

*By $\emptyset$ is meant the set such that $\forall x(x \in \emptyset \leftrightarrow x \neq x)$ i.e. the expression $x \in \emptyset$ is short for the expression $x \neq x$.

*For any set $a$, $\{a\}$ is the set defined thus: $\forall x(x \in \{a\} \leftrightarrow x = a)$ i.e. for any $x$, $x \in \{a\}$ is short for $x = a$. Similarly, $\{a,b\}$ is defined as: $\forall x(x \in \{a,b\} \leftrightarrow (x = a \vee x = b))$. Hence, $x \in \{a,b\}$ is short for $x = a \vee x = b$.

*Now we can define an ordered pair in terms of set theory: for any sets $a$ and $b$, $<a,b>$ is a shorthand for the set $\{\{a\},\{a,b\}\}$. Of course, I could have defined ordered pairs in any way I wanted as long as the definition allows me to choose between the first and second element.

*For classes $A$ and $B$, the class $A \times B$ is defined as the class of all ordered pairs $<y,z>$, where $y$ comes from $A$ and $z$ comes from $B$: $\forall x(x \in A \times B \leftrightarrow \exists y \exists z(y \in A \wedge z \in B \wedge x = <y,z>))$.

*For a set $x$, by $\wp(x)$ we mean the set of all subsets of x i.e. $\forall y(y \in \wp(x) \leftrightarrow y \subseteq x)$ or if you want to replace the $\subseteq$ symbol, $\forall y(y \in \wp(x) \leftrightarrow \forall z(z \in y \to z \in x))$.


Now you have enough material to translate expressions with Cartesian products and power sets into expressions in first-order logic in a straightforward but cumbersome manner:


*

*"if $a = \wp(a)$ then $\wp(a) = \emptyset$" becomes "if $\forall x(x \in a \to x \in \wp(a)) \wedge \forall x(x \in \wp(a) \to x \in a)$ then $\forall x(x \in \wp(a) \to x \in \emptyset) \wedge \forall x(x \in \emptyset \to x \in \wp(a))$" which itself decomposes to "if $\forall x(x \in a \to \forall y(y \in x \to y \in a)) \wedge \forall x(\forall y(y \in x \to y \in a) \to x \in a))$ then $\forall x(\forall y(y \in x \to y \in a) \to x \neq x) \wedge \forall x(x \neq x \to \forall y(y \in x \to y \in a))$".


As you can see, a full translation like that is definitely possible but it is very very tedious! For example, try translating "$A \times B = B \times A$ if and only if $A = B$". It is not fun!
A: There will be differences of opinion about notation, but I like to use:
The Cartesian Product of sets $A$ and $B$ is given by $ A\times B\$ such that:

$\forall x,y:[(x,y)\in A\times B\iff x\in A\land y\in B]$

The power set of set A is given by $\mathcal P(A)$ such that:

$\forall x: [x\in \mathcal P(A)\iff \forall y:[y\in x\implies y\in A]] $

