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 { 𝑥𝐴𝐴 ∈ V } ∈ V

Proof

Step Hyp Ref Expression
1 rabexg ( 𝐴 ∈ V → { 𝑥𝐴𝐴 ∈ V } ∈ V )
2 simpl ( ( ¬ 𝐴 ∈ V ∧ 𝑥𝐴 ) → ¬ 𝐴 ∈ V )
3 2 nrexdv ( ¬ 𝐴 ∈ V → ¬ ∃ 𝑥𝐴 𝐴 ∈ V )
4 rabn0 ( { 𝑥𝐴𝐴 ∈ V } ≠ ∅ ↔ ∃ 𝑥𝐴 𝐴 ∈ V )
5 4 necon1bbii ( ¬ ∃ 𝑥𝐴 𝐴 ∈ V ↔ { 𝑥𝐴𝐴 ∈ V } = ∅ )
6 3 5 sylib ( ¬ 𝐴 ∈ V → { 𝑥𝐴𝐴 ∈ V } = ∅ )
7 0ex ∅ ∈ V
8 6 7 eqeltrdi ( ¬ 𝐴 ∈ V → { 𝑥𝐴𝐴 ∈ V } ∈ V )
9 1 8 pm2.61i { 𝑥𝐴𝐴 ∈ V } ∈ V