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
|- ( ph -> A e. B )
eldifd.2
|- ( ph -> -. A e. C )
Assertion eldifd
|- ( ph -> A e. ( B \ C ) )

Proof

Step Hyp Ref Expression
1 eldifd.1
 |-  ( ph -> A e. B )
2 eldifd.2
 |-  ( ph -> -. A e. C )
3 eldif
 |-  ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )
4 1 2 3 sylanbrc
 |-  ( ph -> A e. ( B \ C ) )