Theorem isset 2732

Description: Two ways to say "𝐴 is a set": A class 𝐴 is a member of the universal class V (see df-v 2728) 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 4415. Note the when 𝐴 is not a set, it is called a proper class. In some theorems, such as uniexg 4417, 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 2161 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 2161	. 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V))
2		vex 2729	. . . 4 ⊢ 𝑥 ∈ V
3	2	biantru 300	. . 3 ⊢ (𝑥 = 𝐴 ↔ (𝑥 = 𝐴 ∧ 𝑥 ∈ V))
4	3	exbii 1593	. 2 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V))
5	1, 4	bitr4i 186	1 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)

Syntax hints:   ∧ wa 103   ↔ wb 104   = wceq 1343  ∃wex 1480   ∈ wcel 2136  Vcvv 2726

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-v 2728

This theorem is referenced by:  issetf  2733  isseti  2734  issetri  2735  elex  2737  elisset  2740  vtoclg1f  2785  ceqex  2853  eueq  2897  moeq  2901  mosubt  2903  ru  2950  sbc5  2974  snprc  3641  vprc  4114  opelopabsb  4238  eusvnfb  4432  euiotaex  5169  fvmptdf  5573  fvmptdv2  5575  fmptco  5651  brabvv  5888  ovmpodf  5973  ovi3  5978  tfrlemibxssdm  6295  tfr1onlembxssdm  6311  tfrcllembxssdm  6324  ecexr  6506  snexxph  6915  bj-vprc  13778  bj-vnex  13780  bj-2inf  13820