Metamath Proof Explorer

Theorem n0rex

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

Ref Expression
Assertion n0rex 
|- ( A =/= (/) -> E. x e. A x e. A )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( x e. A -> x e. A )
2 1 ancli 
 |-  ( x e. A -> ( x e. A /\ x e. A ) )
3 2 eximi 
 |-  ( E. x x e. A -> E. x ( x e. A /\ x e. A ) )
4 n0 
 |-  ( A =/= (/) <-> E. x x e. A )
5 df-rex 
 |-  ( E. x e. A x e. A <-> E. x ( x e. A /\ x e. A ) )
6 3 4 5 3imtr4i 
 |-  ( A =/= (/) -> E. x e. A x e. A )