Metamath Proof Explorer


Theorem eldifd

Description: If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif . (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses eldifd.1 φAB
eldifd.2 φ¬AC
Assertion eldifd φABC

Proof

Step Hyp Ref Expression
1 eldifd.1 φAB
2 eldifd.2 φ¬AC
3 eldif ABCAB¬AC
4 1 2 3 sylanbrc φABC