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	⊢ ( 𝐴 ∈ V ↔ ∃ 𝑥 𝑥 = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		dfclel	⊢ ( 𝐴 ∈ V ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 ∈ V ) )
2		vex	⊢ 𝑥 ∈ V
3	2	biantru	⊢ ( 𝑥 = 𝐴 ↔ ( 𝑥 = 𝐴 ∧ 𝑥 ∈ V ) )
4	3	exbii	⊢ ( ∃ 𝑥 𝑥 = 𝐴 ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝑥 ∈ V ) )
5	1 4	bitr4i	⊢ ( 𝐴 ∈ V ↔ ∃ 𝑥 𝑥 = 𝐴 )