Theorem eldifd 3131

Description: If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif 3130. (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 3130	. 2 |- ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )
4	1, 2, 3	sylanbrc 415	1 |- ( ph -> A e. ( B \ C ) )

Syntax hints:   -. wn 3   -> wi 4   e. wcel 2141   \ cdif 3118

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-dif 3123

This theorem is referenced by:  exmidundif  4192  exmidundifim  4193  frirrg  4335  dcdifsnid  6483  phpelm  6844  findcard2d  6869  findcard2sd  6870  diffifi  6872  unsnfidcex  6897  unsnfidcel  6898  undifdcss  6900  difinfsnlem  7076  difinfsn  7077  hashunlem  10739  seq3coll  10777  fsum3cvg  11341  isumss  11354  fisumss  11355  fproddccvg  11535  fprodssdc  11553  sqrt2irr0  12118  nnoddn2prmb  12216  logbgcd1irr  13679