This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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