Metamath Proof Explorer

Theorem pssnel

Description: A proper subclass has a member in one argument that's not in both. (Contributed by NM, 29-Feb-1996)

Ref Expression
Assertion pssnel 
|- ( A C. B -> E. x ( x e. B /\ -. x e. A ) )

Proof

Step Hyp Ref Expression
1 pssdif 
 |-  ( A C. B -> ( B \ A ) =/= (/) )
2 n0 
 |-  ( ( B \ A ) =/= (/) <-> E. x x e. ( B \ A ) )
3 1 2 sylib 
 |-  ( A C. B -> E. x x e. ( B \ A ) )
4 eldif 
 |-  ( x e. ( B \ A ) <-> ( x e. B /\ -. x e. A ) )
5 4 exbii 
 |-  ( E. x x e. ( B \ A ) <-> E. x ( x e. B /\ -. x e. A ) )
6 3 5 sylib 
 |-  ( A C. B -> E. x ( x e. B /\ -. x e. A ) )