Theorem isset 2741

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

Syntax hints:   ∧ wa 104   ↔ wb 105   = wceq 1353  ∃wex 1490   ∈ wcel 2146  Vcvv 2735

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 1445  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-v 2737

This theorem is referenced by:  issetf  2742  isseti  2743  issetri  2744  elex  2746  elisset  2749  vtoclg1f  2794  ceqex  2862  eueq  2906  moeq  2910  mosubt  2912  ru  2959  sbc5  2984  snprc  3654  snssb  3722  vprc  4130  opelopabsb  4254  eusvnfb  4448  euiotaex  5186  fvmptdf  5595  fvmptdv2  5597  fmptco  5674  brabvv  5911  ovmpodf  5996  ovi3  6001  tfrlemibxssdm  6318  tfr1onlembxssdm  6334  tfrcllembxssdm  6347  ecexr  6530  snexxph  6939  bj-vprc  14188  bj-vnex  14190  bj-2inf  14230