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 xx\in B$$

Proof

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