Metamath Proof Explorer

Theorem ssn0rex

Description: There is an element in a class with a nonempty subclass which is an element of the subclass. (Contributed by AV, 17-Dec-2020)

Ref Expression
Assertion ssn0rex 
|- ( ( A C_ B /\ A =/= (/) ) -> E. x e. B x e. A )

Proof

Step Hyp Ref Expression
1 ssrexv 
 |-  ( A C_ B -> ( E. x e. A x e. A -> E. x e. B x e. A ) )
2 n0rex 
 |-  ( A =/= (/) -> E. x e. A x e. A )
3 1 2 impel 
 |-  ( ( A C_ B /\ A =/= (/) ) -> E. x e. B x e. A )