Metamath Proof Explorer


Theorem elnelneq2d

Description: Two classes are not equal if one but not the other is an element of a given class. (Contributed by Rohan Ridenour, 12-Aug-2023)

Ref Expression
Hypotheses elnelneq2d.1 ( 𝜑𝐴𝐶 )
elnelneq2d.2 ( 𝜑 → ¬ 𝐵𝐶 )
Assertion elnelneq2d ( 𝜑 → ¬ 𝐴 = 𝐵 )

Proof

Step Hyp Ref Expression
1 elnelneq2d.1 ( 𝜑𝐴𝐶 )
2 elnelneq2d.2 ( 𝜑 → ¬ 𝐵𝐶 )
3 simpr ( ( 𝜑𝐴 = 𝐵 ) → 𝐴 = 𝐵 )
4 1 adantr ( ( 𝜑𝐴 = 𝐵 ) → 𝐴𝐶 )
5 3 4 eqeltrrd ( ( 𝜑𝐴 = 𝐵 ) → 𝐵𝐶 )
6 2 5 mtand ( 𝜑 → ¬ 𝐴 = 𝐵 )