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

Proof

Step	Hyp	Ref	Expression
1		neleqtrd.1	|- ( ph -> -. C e. A )
2		neleqtrd.2	|- ( ph -> A = B )
3	2	eleq2d	|- ( ph -> ( C e. A <-> C e. B ) )
4	1 3	mtbid	|- ( ph -> -. C e. B )