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 | |- { A } e. _V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | snsspw | |- { A } C_ ~P A |
|
| 2 | ssexg | |- ( ( { A } C_ ~P A /\ ~P A e. _V ) -> { A } e. _V ) |
|
| 3 | 1 2 | mpan | |- ( ~P A e. _V -> { A } e. _V ) |
| 4 | pwexg | |- ( A e. _V -> ~P A e. _V ) |
|
| 5 | 4 | con3i | |- ( -. ~P A e. _V -> -. A e. _V ) |
| 6 | snprc | |- ( -. A e. _V <-> { A } = (/) ) |
|
| 7 | 6 | biimpi | |- ( -. A e. _V -> { A } = (/) ) |
| 8 | 0ex | |- (/) e. _V |
|
| 9 | 7 8 | eqeltrdi | |- ( -. A e. _V -> { A } e. _V ) |
| 10 | 5 9 | syl | |- ( -. ~P A e. _V -> { A } e. _V ) |
| 11 | 3 10 | pm2.61i | |- { A } e. _V |