Theorem eqneltrrd

Description: If a class is not an element of another class, an equal class is also not an element. Deduction form. (Contributed by David Moews, 1-May-2017) (Proof shortened by Wolf Lammen, 13-Nov-2019)

	Ref	Expression
Hypotheses	eqneltrrd.1	$$⊢\phi \to A=B$$
	eqneltrrd.2	$$⊢\phi \to \neg A\in C$$
Assertion	eqneltrrd	$$⊢\phi \to \neg B\in C$$

Proof

Step	Hyp	Ref	Expression
1		eqneltrrd.1	$$⊢\phi \to A=B$$
2		eqneltrrd.2	$$⊢\phi \to \neg A\in C$$
3	1	eqcomd	$$⊢\phi \to B=A$$
4	3 2	eqneltrd	$$⊢\phi \to \neg B\in C$$