Metamath Proof Explorer

Theorem class2set

Description: Construct, from any class A , 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)

Ref Expression
Assertion class2set ⊢ x ∈ A | A ∈ V ∈ V

Proof

Step Hyp Ref Expression
1 rabexg ⊢ A ∈ V → x ∈ A | A ∈ V ∈ V
2 simpl ⊢ ¬ A ∈ V ∧ x ∈ A → ¬ A ∈ V
3 2 nrexdv ⊢ ¬ A ∈ V → ¬ ∃ x ∈ A A ∈ V
4 rabn0 ⊢ x ∈ A | A ∈ V ≠ ∅ ↔ ∃ x ∈ A A ∈ V
5 4 necon1bbii ⊢ ¬ ∃ x ∈ A A ∈ V ↔ x ∈ A | A ∈ V = ∅
6 3 5 sylib ⊢ ¬ A ∈ V → x ∈ A | A ∈ V = ∅
7 0ex ⊢ ∅ ∈ V
8 6 7 eqeltrdi ⊢ ¬ A ∈ V → x ∈ A | A ∈ V ∈ V
9 1 8 pm2.61i ⊢ x ∈ A | A ∈ V ∈ V