Theorem isset 2780

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

Syntax hints:   ∧ wa 104   ↔ wb 105   = wceq 1373  ∃wex 1516   ∈ wcel 2177  Vcvv 2773

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-v 2775

This theorem is referenced by:  issetf  2781  isseti  2782  issetri  2783  elex  2785  elisset  2788  vtoclg1f  2834  ceqex  2904  eueq  2948  moeq  2952  mosubt  2954  ru  3001  sbc5  3026  snprc  3703  snmb  3759  snssb  3772  vprc  4184  opelopabsb  4314  eusvnfb  4509  elrelimasn  5057  euiotaex  5257  fvmptdf  5680  fvmptdv2  5682  fmptco  5759  brabvv  6004  ovmpodf  6090  ovi3  6096  tfrlemibxssdm  6426  tfr1onlembxssdm  6442  tfrcllembxssdm  6455  ecexr  6638  snexxph  7067  fnpr2ob  13247  bj-vprc  15970  bj-vnex  15972  bj-2inf  16012