Theorem isset 2783

Description: Two ways to say "𝐴 is a set": A class 𝐴 is a member of the universal class V (see df-v 2778) 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 4502. Note the when 𝐴 is not a set, it is called a proper class. In some theorems, such as uniexg 4504, 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 2203 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 2203	. 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V))
2		vex 2779	. . . 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 2178  Vcvv 2776

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 2189

This theorem depends on definitions:  df-bi 117  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-v 2778

This theorem is referenced by:  issetf  2784  isseti  2785  issetri  2786  elex  2788  elisset  2791  vtoclg1f  2837  ceqex  2907  eueq  2951  moeq  2955  mosubt  2957  ru  3004  sbc5  3029  snprc  3708  snmb  3764  snssb  3777  vprc  4192  opelopabsb  4324  eusvnfb  4519  elrelimasn  5067  euiotaex  5267  fvmptdf  5690  fvmptdv2  5692  fmptco  5769  brabvv  6014  ovmpodf  6100  ovi3  6106  tfrlemibxssdm  6436  tfr1onlembxssdm  6452  tfrcllembxssdm  6465  ecexr  6648  snexxph  7078  fnpr2ob  13287  bj-vprc  16031  bj-vnex  16033  bj-2inf  16073