Description: Alternate proof of snex using Power Set ( ax-pow ) instead of Pairing ( ax-pr ). Unlike in the proof of zfpair , Replacement ( ax-rep ) is not needed. (Contributed by NM, 7-Aug-1994) (Proof shortened by Andrew Salmon, 25-Jul-2011) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | snexALT | ⊢ { 𝐴 } ∈ V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | snsspw | ⊢ { 𝐴 } ⊆ 𝒫 𝐴 | |
| 2 | ssexg | ⊢ ( ( { 𝐴 } ⊆ 𝒫 𝐴 ∧ 𝒫 𝐴 ∈ V ) → { 𝐴 } ∈ V ) | |
| 3 | 1 2 | mpan | ⊢ ( 𝒫 𝐴 ∈ V → { 𝐴 } ∈ V ) |
| 4 | pwexg | ⊢ ( 𝐴 ∈ V → 𝒫 𝐴 ∈ V ) | |
| 5 | 4 | con3i | ⊢ ( ¬ 𝒫 𝐴 ∈ V → ¬ 𝐴 ∈ V ) |
| 6 | snprc | ⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ ) | |
| 7 | 6 | biimpi | ⊢ ( ¬ 𝐴 ∈ V → { 𝐴 } = ∅ ) |
| 8 | 0ex | ⊢ ∅ ∈ V | |
| 9 | 7 8 | eqeltrdi | ⊢ ( ¬ 𝐴 ∈ V → { 𝐴 } ∈ V ) |
| 10 | 5 9 | syl | ⊢ ( ¬ 𝒫 𝐴 ∈ V → { 𝐴 } ∈ V ) |
| 11 | 3 10 | pm2.61i | ⊢ { 𝐴 } ∈ V |