Theorem neleqtrd

Description: If a class is not an element of another class, it is also not an element of an equal class. Deduction form. (Contributed by David Moews, 1-May-2017)

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

Proof

Step	Hyp	Ref	Expression
1		neleqtrd.1	$$⊢\phi \to \neg C\in A$$
2		neleqtrd.2	$$⊢\phi \to A=B$$
3	2	eleq2d	$$⊢\phi \to \left(C\in A\leftrightarrow C\in B\right)$$
4	1 3	mtbid	$$⊢\phi \to \neg C\in B$$