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

Metamath Proof Explorer

Theorem elex2

Description: If a class contains another class, then it contains some set. (Contributed by Alan Sare, 25-Sep-2011) Avoid ax-9 , ax-ext , df-clab . (Revised by Wolf Lammen, 30-Nov-2024)

		Ref	Expression
	Assertion	elex2	$⊢ A \in B \to \exists x x \in B$

Proof

Step	Hyp	Ref	Expression
1		dfclel	$⊢ A \in B \leftrightarrow \exists x (x = A \land x \in B)$
2		exsimpr	$⊢ \exists x (x = A \land x \in B) \to \exists x x \in B$
3	1 2	sylbi	$⊢ A \in B \to \exists x x \in B$