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 ⊢ A ∈ V → ∃ x A ∈ x

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ y = A → y ∈ x ↔ A ∈ x
2 1 exbidv ⊢ y = A → ∃ x y ∈ x ↔ ∃ x A ∈ x
3 el ⊢ ∃ x y ∈ x
4 2 3 vtoclg ⊢ A ∈ V → ∃ x A ∈ x