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 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 )