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