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 φ A B
eldifd.2 φ ¬ A C
Assertion eldifd φ A B C


Step Hyp Ref Expression
1 eldifd.1 φ A B
2 eldifd.2 φ ¬ A C
3 eldif A B C A B ¬ A C
4 1 2 3 sylanbrc φ A B C