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	$$⊢\phi \to A\in C$$
	elnelneq2d.2	$$⊢\phi \to \neg B\in C$$
Assertion	elnelneq2d	$$⊢\phi \to \neg A=B$$

Proof

Step	Hyp	Ref	Expression
1		elnelneq2d.1	$$⊢\phi \to A\in C$$
2		elnelneq2d.2	$$⊢\phi \to \neg B\in C$$
3		simpr	$$⊢\left(\phi \wedge A=B\right)\to A=B$$
4	1	adantr	$$⊢\left(\phi \wedge A=B\right)\to A\in C$$
5	3 4	eqeltrrd	$$⊢\left(\phi \wedge A=B\right)\to B\in C$$
6	2 5	mtand	$$⊢\phi \to \neg A=B$$