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 φ A C
elnelneq2d.2 φ ¬ B C
Assertion elnelneq2d φ ¬ A = B

Proof

Step Hyp Ref Expression
1 elnelneq2d.1 φ A C
2 elnelneq2d.2 φ ¬ B C
3 simpr φ A = B A = B
4 1 adantr φ A = B A C
5 3 4 eqeltrrd φ A = B B C
6 2 5 mtand φ ¬ A = B