Theorem isset 1351

Description: Two ways to say "A is a set": A class A is a member of the universal class V (see df-v 1349) 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 1947. Note the when A is not a set, it is called a proper class. In some theorems, such as uniexg 1948, in order to shorten certain proofs we use the 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(s):   x,A

Proof of Theorem isset

Step	Hyp	Ref	Expression
1		df-clel 1099	. 2 ⊢ (A ∈ V ↔ ∃x(x = A ∧ x ∈ V))
2		visset 1350	. . . 4 ⊢ x ∈ V
3	2	biantru 543	. . 3 ⊢ (x = A ↔ (x = A ∧ x ∈ V))
4	3	biex 733	. 2 ⊢ (∃x x = A ↔ ∃x(x = A ∧ x ∈ V))
5	1, 4	bitr4 154	1 ⊢ (A ∈ V ↔ ∃x x = A)

Syntax hints:   ↔ wb 127   ∧ wa 196  ∃wex 678   = wceq 1091   ∈ wcel 1092  Vcvv 1348

This theorem is referenced by:  isseti 1352  issetri 1353  elisset 1354  elex 1356  vtoclgf 1382  cla4gf 1394  ceqex 1410  eueq 1427  moeq 1431  ru 1437  elrabsf 1456  nvelv 1483  snprc 1838  dmsnop 2547  funimaexg 2715  fopab2 2891  tz9.12lem1 3503  tz9.12lem3 3505

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677  ax-9 799  ax-12 802  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349

metamath.org