Theorem eldifd 3176

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

Hypotheses

Ref	Expression
eldifd.1	|- ( ph -> A e. B )
eldifd.2	|- ( ph -> -. A e. C )

Assertion

Ref	Expression
eldifd	|- ( ph -> A e. ( B \ C ) )

Proof of Theorem eldifd

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

Syntax hints:   -. wn 3   -> wi 4   e. wcel 2176   \ cdif 3163

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-dif 3168

This theorem is referenced by:  exmidundif  4251  exmidundifim  4252  frirrg  4398  dcdifsnid  6592  phpelm  6965  findcard2d  6990  findcard2sd  6991  diffifi  6993  unsnfidcex  7019  unsnfidcel  7020  undifdcss  7022  difinfsnlem  7203  difinfsn  7204  hashunlem  10951  seq3coll  10989  fsum3cvg  11722  isumss  11735  fisumss  11736  fproddccvg  11916  fprodssdc  11934  sqrt2irr0  12519  nnoddn2prmb  12618  logbgcd1irr  15472  2lgslem2  15602