Is this expression admitted in ZFC? $A=\{x|x\in A\}$?

Question

The question is expressed in title. Is $``A=\{x|x\in A\}"$ an admitted expression in ZFC.

Answer 1

EDIT: I'm assuming that the OP is asking about whether the expression in question is allowed by the syntax of ZFC, and if so whether it is provable in ZFC. If per Eric Wofsey's comment below the question is instead whether "$A=\{x\vert x\in A\}$" is a valid definition of a set in the ZFC framework (modulo syntax issues), this old answer of mine might be helpful (and the answer is no).

---

No, it's not - set builder notation is not part of the syntax of ZFC. Well-formed formulas in the language of ZFC can only use the logical symbols $\wedge,\vee,\neg,\rightarrow,\leftrightarrow,\exists,\forall,(,),=,$ and the variables, and the non-logical symbol $\in$. Curly braces and $\vert$ are not part of the syntax.

That said, there is a statement expressible in the language of ZFC which essentially does the same job - namely, the axiom of extensionality (which, per the name, is part of ZFC). This says $$\forall a\forall b(a=b\leftrightarrow \forall c(c\in a\leftrightarrow c\in b)),$$ that is, two sets are the same iff they have the same elements. In this sense one may reasonably claim that ZFC does indeed prove that every set is the set of its own elements, but we have to recognize that there's some abuse of notation/terminology going on here.

---

A couple comments:

• First, there's actually a fair amount of flexibility in how we set up the syntax of first-order logic. I've included several Boolean operations ($\wedge,\vee,\neg,\rightarrow,\leftrightarrow$) as primitive, but we don't need to - $\wedge$ and $\neg$ alone, for example, would suffice, or we could use the Sheffer stroke. Similarly, we don't need both $\exists$ and $\forall$. What precise presentation one wants depends on one's purposes: having more primitive symbols makes things easier to write down, but also makes some proofs more annoying by generating more cases. (More interestingly, "$=$" was historically not always considered part of the logical apparatus of first-order logic.)

• Second, note that it's a little unfair to bring up extensionality here since without extensionality set-builder notation doesn't even make sense. Namely, we want to understand "$\{x\vert \varphi(x)\}$" as defining at most one set, but what if there happen to be two distinct sets $a,b$ such that their elements are each everything satisfying $\varphi$? In the absence of extensionality, this could happen - so does $\{x:\varphi(x)\}$ correspond to $a$ or to $b$? Set-builder notation is no longer ambiguous if extensionality fails. So really, I would say that this is a vacuous situation: even ignoring the formal syntax issue, the expression you're looking at doesn't even make sense unless we assume extensionality, in which case it's trivially true.

Answer 2

Informally, whenever you use the set builder notation and want to give the 'built' set a name, say $C$, you write

$$\tag 1 C := {\displaystyle \{x\mid \Phi (x)\}}$$

Informally, once you assign a set to a letter that letter is an object throughout the remainder of the exposition/argument.

The OP already has a letter $A$ reserved for some set. Informally, they can write

$$\tag 2 B := \{x|x\in A\}$$

and claim that $B = A$.

---

In the programming language Python we use

== for =

and

= for :=

Answer 3

If you take set builder notation to translate to a first order formula via $$X=\{x|P(x)\} ≡ ∀x. (x∈X⇔P(x))$$

and with $P(x)$ denoting $x\in X$, then your question is answered positively by the observation that there's nothing wrong with

$$∀x. (x∈X⇔x∈X).$$

It's even true. Although your question doesn't speak about provability, just about expression.
You can also introduce extra notations narrowing down on any axioms and you still got a first-order theory with equality $=$.

Since other answers also pointed towards various related bits of information, and since you're in search of restrictions, one may note that in standard the Axiom_schema_of_specification, $$\forall X.\,\exists Y.\,\forall x.(x\in A\Leftrightarrow \phi(x, A))$$ the the term variable $B$ ought to be not free in the predicate $\phi$.