Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  class2set Structured version   Visualization version   GIF version

Theorem class2set 5242
 Description: Construct, from any class 𝐴, a set equal to it when the class exists and equal to the empty set when the class is proper. This theorem shows that the constructed set always exists. (Contributed by NM, 16-Oct-2003.)
Assertion
Ref Expression
class2set {𝑥𝐴𝐴 ∈ V} ∈ V
Distinct variable group:   𝑥,𝐴

Proof of Theorem class2set
StepHypRef Expression
1 rabexg 5221 . 2 (𝐴 ∈ V → {𝑥𝐴𝐴 ∈ V} ∈ V)
2 simpl 486 . . . . 5 ((¬ 𝐴 ∈ V ∧ 𝑥𝐴) → ¬ 𝐴 ∈ V)
32nrexdv 3263 . . . 4 𝐴 ∈ V → ¬ ∃𝑥𝐴 𝐴 ∈ V)
4 rabn0 4322 . . . . 5 ({𝑥𝐴𝐴 ∈ V} ≠ ∅ ↔ ∃𝑥𝐴 𝐴 ∈ V)
54necon1bbii 3063 . . . 4 (¬ ∃𝑥𝐴 𝐴 ∈ V ↔ {𝑥𝐴𝐴 ∈ V} = ∅)
63, 5sylib 221 . . 3 𝐴 ∈ V → {𝑥𝐴𝐴 ∈ V} = ∅)
7 0ex 5198 . . 3 ∅ ∈ V
86, 7eqeltrdi 2924 . 2 𝐴 ∈ V → {𝑥𝐴𝐴 ∈ V} ∈ V)
91, 8pm2.61i 185 1 {𝑥𝐴𝐴 ∈ V} ∈ V
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   = wceq 1538   ∈ wcel 2115  ∃wrex 3134  {crab 3137  Vcvv 3480  ∅c0 4276 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5190  ax-nul 5197 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-dif 3922  df-in 3926  df-ss 3936  df-nul 4277 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator