Theorem isset 2820

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

Syntax hints:   ∧ wa 104   ↔ wb 105   = wceq 1398  ∃wex 1541   ∈ wcel 2203  Vcvv 2813

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-v 2815

This theorem is referenced by:  issetf  2821  isseti  2822  issetri  2823  elex  2825  elisset  2828  vtoclg1f  2874  ceqex  2944  eueq  2988  moeq  2992  mosubt  2994  ru  3041  sbc5  3066  snprc  3754  rabsnif  3758  snmb  3813  snssb  3827  vprc  4242  opelopabsb  4378  eusvnfb  4575  elrelimasn  5128  euiotaex  5329  fvmptdf  5765  fvmptdv2  5767  fmptco  5843  brabvv  6099  ovmpodf  6185  ovi3  6191  tfrlemibxssdm  6558  tfr1onlembxssdm  6574  tfrcllembxssdm  6587  ecexr  6772  snexxph  7220  fnpr2ob  13553  bj-vprc  16666  bj-vnex  16668  bj-2inf  16708