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 e. B -> E. x x e. B )

Proof

Step	Hyp	Ref	Expression
1		dfclel	|- ( A e. B <-> E. x ( x = A /\ x e. B ) )
2		exsimpr	|- ( E. x ( x = A /\ x e. B ) -> E. x x e. B )
3	1 2	sylbi	|- ( A e. B -> E. x x e. B )