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

Theorem class2set 4657
 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 4638 . 2 (𝐴 ∈ V → {𝑥𝐴𝐴 ∈ V} ∈ V)
2 simpl 471 . . . . 5 ((¬ 𝐴 ∈ V ∧ 𝑥𝐴) → ¬ 𝐴 ∈ V)
32nrexdv 2888 . . . 4 𝐴 ∈ V → ¬ ∃𝑥𝐴 𝐴 ∈ V)
4 rabn0 3815 . . . . 5 ({𝑥𝐴𝐴 ∈ V} ≠ ∅ ↔ ∃𝑥𝐴 𝐴 ∈ V)
54necon1bbii 2735 . . . 4 (¬ ∃𝑥𝐴 𝐴 ∈ V ↔ {𝑥𝐴𝐴 ∈ V} = ∅)
63, 5sylib 206 . . 3 𝐴 ∈ V → {𝑥𝐴𝐴 ∈ V} = ∅)
7 0ex 4617 . . 3 ∅ ∈ V
86, 7syl6eqel 2600 . 2 𝐴 ∈ V → {𝑥𝐴𝐴 ∈ V} ∈ V)
91, 8pm2.61i 174 1 {𝑥𝐴𝐴 ∈ V} ∈ V
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   = wceq 1474   ∈ wcel 1938  ∃wrex 2801  {crab 2804  Vcvv 3077  ∅c0 3777 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616 This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3079  df-dif 3447  df-in 3451  df-ss 3458  df-nul 3778 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator