Metamath Proof Explorer

Theorem elnelne1

Description: Two classes are different if they don't contain the same element. (Contributed by AV, 28-Jan-2020)

Ref Expression
Assertion elnelne1 
|- ( ( A e. B /\ A e/ C ) -> B =/= C )

Proof

Step Hyp Ref Expression
1 df-nel 
 |-  ( A e/ C <-> -. A e. C )
2 nelne1 
 |-  ( ( A e. B /\ -. A e. C ) -> B =/= C )
3 1 2 sylan2b 
 |-  ( ( A e. B /\ A e/ C ) -> B =/= C )