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

Theorem class2set 4960
 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 4942 . 2 (𝐴 ∈ V → {𝑥𝐴𝐴 ∈ V} ∈ V)
2 simpl 468 . . . . 5 ((¬ 𝐴 ∈ V ∧ 𝑥𝐴) → ¬ 𝐴 ∈ V)
32nrexdv 3148 . . . 4 𝐴 ∈ V → ¬ ∃𝑥𝐴 𝐴 ∈ V)
4 rabn0 4102 . . . . 5 ({𝑥𝐴𝐴 ∈ V} ≠ ∅ ↔ ∃𝑥𝐴 𝐴 ∈ V)
54necon1bbii 2991 . . . 4 (¬ ∃𝑥𝐴 𝐴 ∈ V ↔ {𝑥𝐴𝐴 ∈ V} = ∅)
63, 5sylib 208 . . 3 𝐴 ∈ V → {𝑥𝐴𝐴 ∈ V} = ∅)
7 0ex 4921 . . 3 ∅ ∈ V
86, 7syl6eqel 2857 . 2 𝐴 ∈ V → {𝑥𝐴𝐴 ∈ V} ∈ V)
91, 8pm2.61i 176 1 {𝑥𝐴𝐴 ∈ V} ∈ V
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   = wceq 1630   ∈ wcel 2144  ∃wrex 3061  {crab 3064  Vcvv 3349  ∅c0 4061 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-sep 4912  ax-nul 4920 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ne 2943  df-ral 3065  df-rex 3066  df-rab 3069  df-v 3351  df-dif 3724  df-in 3728  df-ss 3735  df-nul 4062 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator