Theorem isset 2807

Description: Two ways to say "𝐴 is a set": A class 𝐴 is a member of the universal class V (see df-v 2802) if and only if the class 𝐴 exists (i.e. there exists some set 𝑥 equal to class 𝐴). Theorem 6.9 of [Quine] p. 43. Notational convention: We will use the notational device "𝐴 ∈ V " to mean "𝐴 is a set" very frequently, for example in uniex 4532. Note the when 𝐴 is not a set, it is called a proper class. In some theorems, such as uniexg 4534, in order to shorten certain proofs we use the more general antecedent 𝐴 ∈ 𝑉 instead of 𝐴 ∈ V to mean "𝐴 is a set."

Note that a constant is implicitly considered distinct from all variables. This is why V is not included in the distinct variable list, even though df-clel 2225 requires that the expression substituted for 𝐵 not contain 𝑥. (Also, the Metamath spec does not allow constants in the distinct variable list.) (Contributed by NM, 26-May-1993.)

Assertion

Ref	Expression
isset	⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)

Distinct variable group:   𝑥,𝐴

Proof of Theorem isset

Step	Hyp	Ref	Expression
1		df-clel 2225	. 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V))
2		vex 2803	. . . 4 ⊢ 𝑥 ∈ V
3	2	biantru 302	. . 3 ⊢ (𝑥 = 𝐴 ↔ (𝑥 = 𝐴 ∧ 𝑥 ∈ V))
4	3	exbii 1651	. 2 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V))
5	1, 4	bitr4i 187	1 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)

Syntax hints:   ∧ wa 104   ↔ wb 105   = wceq 1395  ∃wex 1538   ∈ wcel 2200  Vcvv 2800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-v 2802

This theorem is referenced by:  issetf  2808  isseti  2809  issetri  2810  elex  2812  elisset  2815  vtoclg1f  2861  ceqex  2931  eueq  2975  moeq  2979  mosubt  2981  ru  3028  sbc5  3053  snprc  3732  rabsnif  3736  snmb  3791  snssb  3804  vprc  4219  opelopabsb  4352  eusvnfb  4549  elrelimasn  5100  euiotaex  5301  fvmptdf  5730  fvmptdv2  5732  fmptco  5809  brabvv  6062  ovmpodf  6148  ovi3  6154  tfrlemibxssdm  6488  tfr1onlembxssdm  6504  tfrcllembxssdm  6517  ecexr  6702  snexxph  7140  fnpr2ob  13413  bj-vprc  16427  bj-vnex  16429  bj-2inf  16469