Metamath Proof Explorer

Theorem class2set

Description: The class of elements of A "such that A is a set" is a set. That class is equal to A when A is a set (see class2seteq ) and to the empty set when A is a proper class. (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