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 φ¬CA
neleqtrd.2 φA=B
Assertion neleqtrd φ¬CB

Proof

Step Hyp Ref Expression
1 neleqtrd.1 φ¬CA
2 neleqtrd.2 φA=B
3 2 eleq2d φCACB
4 1 3 mtbid φ¬CB