Theorem isset 2809

Description: Two ways to say "𝐴 is a set": A class 𝐴 is a member of the universal class V (see df-v 2804) 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 4534. Note the when 𝐴 is not a set, it is called a proper class. In some theorems, such as uniexg 4536, 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 2227 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 2227	. 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V))
2		vex 2805	. . . 4 ⊢ 𝑥 ∈ V
3	2	biantru 302	. . 3 ⊢ (𝑥 = 𝐴 ↔ (𝑥 = 𝐴 ∧ 𝑥 ∈ V))
4	3	exbii 1653	. 2 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V))
5	1, 4	bitr4i 187	1 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)

Syntax hints:   ∧ wa 104   ↔ wb 105   = wceq 1397  ∃wex 1540   ∈ wcel 2202  Vcvv 2802

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-v 2804

This theorem is referenced by:  issetf  2810  isseti  2811  issetri  2812  elex  2814  elisset  2817  vtoclg1f  2863  ceqex  2933  eueq  2977  moeq  2981  mosubt  2983  ru  3030  sbc5  3055  snprc  3734  rabsnif  3738  snmb  3793  snssb  3806  vprc  4221  opelopabsb  4354  eusvnfb  4551  elrelimasn  5102  euiotaex  5303  fvmptdf  5734  fvmptdv2  5736  fmptco  5813  brabvv  6066  ovmpodf  6152  ovi3  6158  tfrlemibxssdm  6492  tfr1onlembxssdm  6508  tfrcllembxssdm  6521  ecexr  6706  snexxph  7148  fnpr2ob  13422  bj-vprc  16491  bj-vnex  16493  bj-2inf  16533