Metamath Proof Explorer

Theorem elex2

Description: If a class contains another class, then it contains some set. (Contributed by Alan Sare, 25-Sep-2011)

Ref Expression
Assertion elex2 
|- ( A e. B -> E. x x e. B )

Proof

Step Hyp Ref Expression
1 eleq1a 
 |-  ( A e. B -> ( x = A -> x e. B ) )
2 1 alrimiv 
 |-  ( A e. B -> A. x ( x = A -> x e. B ) )
3 elisset 
 |-  ( A e. B -> E. x x = A )
4 exim 
 |-  ( A. x ( x = A -> x e. B ) -> ( E. x x = A -> E. x x e. B ) )
5 2 3 4 sylc 
 |-  ( A e. B -> E. x x e. B )