Metamath Proof Explorer

Theorem bj-n0i

Description: Inference associated with n0 . Shortens 2ndcdisj (2888>2878), notzfaus (264>253). (Contributed by BJ, 22-Apr-2019)

Ref Expression
Hypothesis bj-n0i.1 
|- A =/= (/)
Assertion bj-n0i 
|- E. x x e. A

Proof

Step Hyp Ref Expression
1 bj-n0i.1 
 |-  A =/= (/)
2 n0 
 |-  ( A =/= (/) <-> E. x x e. A )
3 1 2 mpbi 
 |-  E. x x e. A