Theorem isset 1811

Description: Two ways to say "A is a set": A class A is a member of the universal class V (see df-v 1809) 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. Notational convention: We will use the notational device "A ∈ V" to mean "A is a set" very frequently, for example in uniex 2866. Note the when A is not a set, it is called a proper class. In some theorems, such as uniexg 2867, in order to shorten certain proofs we use the more general antecedent A ∈ B instead of A ∈ V to mean "A is a set."

Assertion

Ref	Expression
isset	⊢ (A ∈ V ↔ ∃x x = A)

Distinct variable group:   x,A

Proof of Theorem isset

Step	Hyp	Ref	Expression
1		df-clel 1471	. 2 ⊢ (A ∈ V ↔ ∃x(x = A ⋀ x ∈ V))
2		visset 1810	. . . 4 ⊢ x ∈ V
3	2	biantru 723	. . 3 ⊢ (x = A ↔ (x = A ⋀ x ∈ V))
4	3	exbii 1050	. 2 ⊢ (∃x x = A ↔ ∃x(x = A ⋀ x ∈ V))
5	1, 4	bitr4 176	1 ⊢ (A ∈ V ↔ ∃x x = A)

Syntax hints:   ↔ wb 146   ⋀ wa 223   = wceq 955   ∈ wcel 957  ∃wex 979  Vcvv 1808

This theorem is referenced by:  isseti 1812  issetri 1813  elisset 1814  elex 1816  vtoclgf 1843  cla4gf 1857  ceqex 1883  eueq 1913  moeq 1917  ru 1935  elrabsf 1960  snprc 2440  nvelv 2709  vnex 2711  dmsnop 3324  funimaexg 3571  isarep2 3574  fopab2 3818  tz9.12lem1 4642  tz9.12lem3 4644

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471  df-v 1809

Copyright terms: Public domain