Description: Alternate proof of sels , requiring ax-sep but not using el (which is proved from it as elALT ). (especially when the proof of el is inlined in sels ). (Contributed by NM, 4-Jan-2002) Generalize from the proof of elALT . (Revised by BJ, 3-Apr-2019) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | selsALT | |- ( A e. V -> E. x A e. x ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | snidg | |- ( A e. V -> A e. { A } ) |
|
2 | snexg | |- ( A e. { A } -> { A } e. _V ) |
|
3 | snidg | |- ( A e. { A } -> A e. { A } ) |
|
4 | eleq2 | |- ( x = { A } -> ( A e. x <-> A e. { A } ) ) |
|
5 | 2 3 4 | spcedv | |- ( A e. { A } -> E. x A e. x ) |
6 | 1 5 | syl | |- ( A e. V -> E. x A e. x ) |