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	|- ( ph -> A e. C )
	elnelneq2d.2	|- ( ph -> -. B e. C )
Assertion	elnelneq2d	|- ( ph -> -. A = B )

Proof

Step	Hyp	Ref	Expression
1		elnelneq2d.1	|- ( ph -> A e. C )
2		elnelneq2d.2	|- ( ph -> -. B e. C )
3		simpr	|- ( ( ph /\ A = B ) -> A = B )
4	1	adantr	|- ( ( ph /\ A = B ) -> A e. C )
5	3 4	eqeltrrd	|- ( ( ph /\ A = B ) -> B e. C )
6	2 5	mtand	|- ( ph -> -. A = B )