Theorem isset

Description: Two ways to express that " A is a set": A class A is a member of the universal class _V (see df-v ) if and only if the class A exists (i.e., there exists some set x equal to class A ). Theorem 6.9 of Quine p. 43.

A class A which is not a set is called aproper class.

Conventions: We will often use the expression " A e.V " to mean " A is a set", for example in uniex . To make some theorems more readily applicable, we will also use the more general expression A e. V instead of A e. V to mean " A is a set", typically in an antecedent, or in a hypothesis for theorems in deduction form (see for instance uniexg compared with uniex ). That this is more general is seen either by substitution (when the variable V has no other occurrences), or by elex . (Contributed by NM, 26-May-1993)

	Ref	Expression
Assertion	isset	$$⊢A\in \mathrm{V}\leftrightarrow \exists xx=A$$

Proof

Step	Hyp	Ref	Expression
1		dfclel	$$⊢A\in \mathrm{V}\leftrightarrow \exists x\left(x=A\wedge x\in \mathrm{V}\right)$$
2		vex	$$⊢x\in \mathrm{V}$$
3	2	biantru	$$⊢x=A\leftrightarrow \left(x=A\wedge x\in \mathrm{V}\right)$$
4	3	exbii	$$⊢\exists xx=A\leftrightarrow \exists x\left(x=A\wedge x\in \mathrm{V}\right)$$
5	1 4	bitr4i	$$⊢A\in \mathrm{V}\leftrightarrow \exists xx=A$$