Metamath Proof Explorer


Theorem selsALT

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 ( 𝐴𝑉 → ∃ 𝑥 𝐴𝑥 )

Proof

Step Hyp Ref Expression
1 snidg ( 𝐴𝑉𝐴 ∈ { 𝐴 } )
2 snexg ( 𝐴 ∈ { 𝐴 } → { 𝐴 } ∈ V )
3 snidg ( 𝐴 ∈ { 𝐴 } → 𝐴 ∈ { 𝐴 } )
4 eleq2 ( 𝑥 = { 𝐴 } → ( 𝐴𝑥𝐴 ∈ { 𝐴 } ) )
5 2 3 4 spcedv ( 𝐴 ∈ { 𝐴 } → ∃ 𝑥 𝐴𝑥 )
6 1 5 syl ( 𝐴𝑉 → ∃ 𝑥 𝐴𝑥 )