Metamath Proof Explorer

Theorem neleqtrrd

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) (Proof shortened by Wolf Lammen, 13-Nov-2019)

Ref Expression
Hypotheses neleqtrrd.1 φ ¬ C B
neleqtrrd.2 φ A = B
Assertion neleqtrrd φ ¬ C A


Step Hyp Ref Expression
1 neleqtrrd.1 φ ¬ C B
2 neleqtrrd.2 φ A = B
3 2 eqcomd φ B = A
4 1 3 neleqtrd φ ¬ C A