Theorem isset 2616

Description: Two ways to say "𝐴 is a set": A class 𝐴 is a member of the universal class V (see df-v 2614) 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 4228. Note the when 𝐴 is not a set, it is called a proper class. In some theorems, such as uniexg 4229, 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 2079 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 2079	. 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V))
2		vex 2615	. . . 4 ⊢ 𝑥 ∈ V
3	2	biantru 296	. . 3 ⊢ (𝑥 = 𝐴 ↔ (𝑥 = 𝐴 ∧ 𝑥 ∈ V))
4	3	exbii 1537	. 2 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V))
5	1, 4	bitr4i 185	1 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)

Syntax hints:   ∧ wa 102   ↔ wb 103   = wceq 1285  ∃wex 1422   ∈ wcel 1434  Vcvv 2612

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-ext 2065

This theorem depends on definitions:  df-bi 115  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-v 2614

This theorem is referenced by:  issetf  2617  isseti  2618  issetri  2619  elex  2621  elisset  2624  ceqex  2732  eueq  2774  moeq  2778  mosubt  2780  ru  2825  sbc5  2849  snprc  3481  vprc  3936  opelopabsb  4051  eusvnfb  4240  euiotaex  4950  fvmptdf  5335  fvmptdv2  5337  fmptco  5406  brabvv  5630  ovmpt2df  5711  ovi3  5716  tfrlemibxssdm  6024  tfr1onlembxssdm  6040  tfrcllembxssdm  6053  ecexr  6227  snexxph  6583  bj-vprc  11130  bj-vnex  11132  bj-2inf  11176