This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ ( 𝜑 → ¬ 𝐶 ∈ 𝐴 )
	neleqtrd.2	⊢ ( 𝜑 → 𝐴 = 𝐵 )
Assertion	neleqtrd	⊢ ( 𝜑 → ¬ 𝐶 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		neleqtrd.1	⊢ ( 𝜑 → ¬ 𝐶 ∈ 𝐴 )
2		neleqtrd.2	⊢ ( 𝜑 → 𝐴 = 𝐵 )
3	2	eleq2d	⊢ ( 𝜑 → ( 𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵 ) )
4	1 3	mtbid	⊢ ( 𝜑 → ¬ 𝐶 ∈ 𝐵 )