Logical form of family of sets/ power set I am working through Daniel Velleman's How To Prove It, but I am having difficulty understanding the given solution. I am asked to translate the following into a logical form (one which explicates set membership with predicate logic):
$$ B\in\{ \mathscr P(A) | A\in\mathcal F\}  $$
where $$\mathscr P(A)$$ is the power set of A and
$$\mathcal F $$ is a family of sets.
$$ B\in\{ \mathscr P(A) | A\in\mathcal F\}  $$ as proven in earlier page, just means $$\exists A\in\mathcal F (B=\mathscr P(A))$$
And the equal sign just means $$ \forall x (x\in B \iff x\in \mathscr P(A)) $$ On the other hand,
$$ x\in \mathscr P(A)$$ just means x is a subset of A, where $$\forall y(y \in x \to y\in A) $$.
Thus my answer is this: $$\exists A\in\mathcal F\forall y(y\in B \iff y \in x \to y \in A) $$
But the answer given is this:
$$\exists A\in\mathcal F\forall x(x\in B \iff \forall y(y \in x \to y \in A)) $$
I know all he did was substituting $$ x\in \mathscr P(A)$$ with $$\forall y(y \in x \to y\in A) $$ but the $$\forall x(x\in B$$ really bugs me. Firstly, since x is an element of the powerset, it must be a set by definition. So why the universal quantifier? 
Secondly, and this is the most important point, the answer given on the whole just doesn't look like a subset membership formula you normally see. Instead of saying 'All elements of B also belong to the powerset of A', this is saying anything but.
Could anyone please help clarify the thinking behind the given answer and verify if my own answer is correct please? Thank you so much! (Pardon my spacing, I am still learning how to use MathJax)
 A: happy to help.
This is my first post here, so I will write as many as I can to follow the arguments and to learn to write in TeX. I'm sorry it took 4 years for you to get an answer. Let me start by mentioning that I do not like to present a logic form in this way: $$\forall x P(x) \text{ or } \forall x \in U P(x)$$ I prefer this way, because it helps me with more complex forms: $$(\forall x) [P(x)] \text{ or } (\forall x \in U)[P(x)]$$
InVelleman's book, he mentions that the truth set of a statement P(x) can be defined by $$\text{Truth set of }P(x) = \{x \mid P(x)\}$$or, by using the universe of discourse where x is defined: $\text{Truth set of }P(x) = \{x \in U \mid P(x)\}$
He defines the statement $P(x)$ as an elementhood test for a set (any value of $x$ that makes this statement come out true passes the test and is an element of the set).
He defines that the statement $P(x)$ can also be used in a different form. Suppose that $P(x)$ is $x^2<9$. Thus, with the set notation, we have $\{x \mid x^2<9\}$. Now, let's merge this idea with the element hood test. We can show in a broad way of thinking that an element could\could not be part of this set by writing it as $y\in\{x\;|\;x^2<9\}$ or $y\notin\{x \mid x^2<9\}$ ($y$ is called a free variable, whereas $x$ is a bound variable).
Note that, in this case, writing $y\in\{x \mid x^2<9\}$ is the same as writing $P(y)$, because $y$ are the values that make the set true for the given statement $P(x)$. Therefore, since now we know exactly which elements belong to a set, i.e., make this statement come out true, we can assign a capital letter, for example, $A$ to it: $$A=\{x \mid x^2<9\}\,\;or\;A=\{x \in U \mid x^2<9\}$$ (if there was any possibility of confusion about what the universe was, we could specify it explicitly by writing the $U$)
Velleman, however, notes that sometimes we don't want to pay attention to the universe of discourse $U$ when we are talking about logical forms, but rather to restrict attention to a subset of $U$. In this way, we would have the following:
$$(\forall x \in U)[P(x)] \text{ is transformed into }(\forall x \in U) \{(\exists y \in U)[P(x,y)]\}$$
In this case, the values of $y$ would make this restricted statement about $x$ true. An example would be the statement: Let's think about the set S of perfect squares. This would be the same as restricting the set of real numbers $x$ to the set of only the real numbers that are perfect squares, i.e., that are the square of $n$, where $n$ is a natural number (his convention is to include the 0 in the set of natural numbers). So, the logical form would be: 
$$(\forall x \in \mathbb{R})[P(x \text{ is a perfect square})] \text{ is transformed into }(\forall x \in \mathbb{R}) \{(\exists n \in \mathbb{N})[x=n^2]\}$$
As an abbreviation, we have:
$$(\forall x)[P(x \text{ is a perfect square})] \text{ is transformed into }(\forall x) \{(\exists n \in \mathbb{N})[x=n^2]\}$$
Note that the values of $x$ that are restricted only to be perfect numbers come from the validity of the universe of $n$ when $[x=n^2]$ is true. In this case, the values of $x$ will be natural numbers as well.
Also, he proposes what he calls a more complex set notation that helps when we want to express some statement that restricts the universe of discourse:
$$\{x \mid P(x)\} \text{ is transformed into } \{n^2 \mid n \in \mathbb{N}\}$$
Let's follow the logic to the example Let's think about the set S of perfect squares and see how does he get to the final form:
i) We transform the statement "set of perfect squares" into: a set in which elements are of the form $n^2$, where $n$ is a natural number. Then, we would have the following set notation transformation:
$$\text{Truth set of }P(x) = \{x \mid P(x)\} \text{ is transformed into } S=\{n^2 \mid n \in \mathbb{N}\}$$
ii) Since we are interested in values of $x$ that represent perfect squares, we set $x$ equal to $n^2$ and complete the logical form by using the idea of restricting $U$ that we just learned.
$$(\forall x)[P(x \text{ is a perfect square})] \text{ is transformed into }(\forall x) \{(\exists n)[x=n^2]\}$$
iii) Bringing both ideas together, we can say that 
$$x \text{ was transformed into } n^2$$
$$n \in \mathbb{N} \text{ was transformed into } (\exists n \in \mathbb{N})[x=n^2]$$
Note that $(\exists n \in \mathbb{N})[x=n^2]$ express the values of $x$ that makes the statement set of perfect squares true. So, as we mentioned, it is the same as $P(x)$. Thus, we can also express $(\exists n \in \mathbb{N})[x=n^2]$ in the elementhood test notation:
$$(\exists n \in \mathbb{N})[x=n^2] \text{ means } x \in \{n^2 \mid n \in \mathbb{N}\}$$
Going back to your question and applying what we learned here, we have to construct the idea: $$B\in\{ \mathscr P(A) | A\in\mathcal F\}$$
i) We are looking at the values of $B$ that makes some statement true. Which statement is that?
In the previous example, $x$ took the form of $n^2$, and then we had that $x=n^2$. So the statement was "set of perfect squares". So we were looking at elements that are perfect squares, where $n \in \mathbb{N}$ restricted our $U$ (real numbers) to perfect squares (i.e., values of $x$) that came from natural numbers only, avoiding things such as $2.25=1.5^2$.
Here, $B$ takes the form of $\mathscr P(A)$, so $B=\mathscr P(A)$. So the statement is "B is the power set of A", where $A \in \mathcal F$ imposes a restriction on our $U$ (which is $\mathscr P(A)$) that $A$ needs to be in some particular $\mathcal F$, where $\mathcal F$ is just a family of sets, in which the sets are the elements of $\mathscr P(A)$ since it is implicit in the exercise that $\mathcal F \subseteq \mathscr P(A)$.
So, from what we saw in (iii):
$$B\in\{ \mathscr P(A) | A\in\mathcal F\} \text{ means } (\exists A \in \mathcal F)[B=\mathscr P(A)]$$
ii) Now, we need to rewrite $[B=\mathscr P(A)]$ in the logical form, using the bound variable $X$ (I prefer to use capital letter $X$):
$$\forall X (X\in B \iff X\in \mathscr P(A))$$
iii) So far, we have:
$$(\exists A \in \mathcal F)[\forall X (X\in B \iff X\in \mathscr P(A))]$$
Note that your problem appears now. $X$ is implicitly mentioning a universe of discourse $U$, which are all possible elements of $\mathscr P(A)$, which are subsets of $A$.
iv) Let's put $X\in \mathscr P(A)$ in its logical form, using the bound variable $y$:
$$\forall y(y \in X \to y\in A)$$
At the same time, Velleman follows a convention of using different bound variables when one bound variable ($X$) talks about one thing ( being in $B$) and the other ($y$) talks about another thing (being in $X$).
$$(\exists A \in \mathcal F)[\forall X (X\in B \iff \forall y(y \in X \to y\in A))]$$
To conclude, the universe of discourse of $X$ is $\mathscr P(A)$ but the universe of discourse of $y$ is $A$, so $X$ and $y$ need to be quantifying over different bound variables.
$$(\exists A \in \mathcal F)\{(\forall X \in \mathscr P(A))[X\in B \iff (\forall y \in A)[y \in X \to y\in A]]\}$$
I hope it helps. Does anyone else have any opinion on this reasoning?
A: In set theory nothing prevents from quantifiying over sets. 
Remember that in standard axiomatic set theory, all the objects you are talking about are sets, there is no " pure element". So, if you use quantifiers, you have to quantify over sets. 
The universal quantifyer that bothers you is precisely here to translate an inclusion statement. 

