Theorem isset 3335

Description: Two ways to say "𝐴 is a set": A class 𝐴 is a member of the universal class V (see df-v 3330) 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 7106. Note that a class 𝐴 which is not a set is called a proper class. In some theorems, such as uniexg 7108, 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 2744 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 2744	. 2 ⊢ (𝐴 ∈ V ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V))
2		vex 3331	. . . 4 ⊢ 𝑥 ∈ V
3	2	biantru 527	. . 3 ⊢ (𝑥 = 𝐴 ↔ (𝑥 = 𝐴 ∧ 𝑥 ∈ V))
4	3	exbii 1911	. 2 ⊢ (∃𝑥 𝑥 = 𝐴 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ V))
5	1, 4	bitr4i 267	1 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)

Syntax hints:   ↔ wb 196   ∧ wa 383   = wceq 1620  ∃wex 1841   ∈ wcel 2127  Vcvv 3328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-12 2184  ax-ext 2728

This theorem depends on definitions:  df-bi 197  df-an 385  df-tru 1623  df-ex 1842  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-v 3330

This theorem is referenced by:  issetf  3336  isseti  3337  issetri  3338  elex  3340  elisset  3343  vtoclg1f  3393  eueq  3507  moeq  3511  ru  3563  sbc5  3589  snprc  4385  vprc  4936  vnex  4938  eusvnfb  4999  reusv2lem3  5008  iotaex  6017  funimaexg  6124  fvmptd3f  6445  fvmptdv2  6448  ovmpt2df  6945  rankf  8818  isssc  16652  dmscut  32195  snelsingles  32306  bj-snglex  33238  bj-nul  33295  dissneqlem  33469  iotaexeu  39090  elnev  39110  ax6e2nd  39245  ax6e2ndVD  39612  ax6e2ndALT  39634  upbdrech  39987  itgsubsticclem  40663