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

Metamath Proof Explorer

Theorem sels

Description: If a class is a set, then it is a member of a set. (Contributed by NM, 4-Jan-2002) Generalize from the proof of elALT . (Revised by BJ, 3-Apr-2019) Avoid ax-sep , ax-nul , ax-pow . (Revised by BTernaryTau, 15-Jan-2025)

		Ref	Expression
	Assertion	sels	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 𝐴 ∈ 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		eleq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥 ) )
2	1	exbidv	⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑥 𝑦 ∈ 𝑥 ↔ ∃ 𝑥 𝐴 ∈ 𝑥 ) )
3		el	⊢ ∃ 𝑥 𝑦 ∈ 𝑥
4	2 3	vtoclg	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 𝐴 ∈ 𝑥 )