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

Metamath Proof Explorer

Theorem eqneltri

Description: If a class is not an element of another class, an equal class is also not an element. (Contributed by Glauco Siliprandi, 3-Jan-2021)

Ref Expression
Hypotheses eqneltri.1 ⊢ 𝐴 = 𝐵
eqneltri.2 ⊢ ¬ 𝐵 ∈ 𝐶
Assertion eqneltri ¬ 𝐴 ∈ 𝐶

Proof

Step Hyp Ref Expression
1 eqneltri.1 ⊢ 𝐴 = 𝐵
2 eqneltri.2 ⊢ ¬ 𝐵 ∈ 𝐶
3 1 eleq1i ⊢ ( 𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶 )
4 2 3 mtbir ⊢ ¬ 𝐴 ∈ 𝐶