Theorem eldifd 3487

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

Syntax hints:   -. wn 3   -> wi 4   e. wcel 1767   \ cdif 3473

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-dif 3479

This theorem is referenced by:  xpdifid  5433  ressuppssdif  6918  oaf1o  7209  findcard2d  7758  cantnflem1  8104  cantnflem2  8105  cantnflem1OLD  8127  fin23lem26  8701  isf34lem4  8753  isfin7-2  8772  axdc3lem4  8829  axdc4lem  8831  ttukeylem7  8891  pwfseqlem1  9032  pwfseqlem3  9034  hashf1lem1  12466  seqcoll  12474  seqcoll2  12475  rlimcld2  13360  sumrblem  13492  fsumcvg  13493  fsumss  13506  incexclem  13607  ruclem12  13831  prmreclem5  14293  ramub1lem1  14399  mreexd  14893  frgpnabllem1  16668  gsumzaddlem  16725  gsumzaddlemOLD  16727  gsum2d  16790  gsum2dOLD  16791  dmdprdsplitlem  16874  dmdprdsplitlemOLD  16875  pgpfac1lem2  16916  pgpfac1lem3  16918  irredrmul  17140  lsppratlem3  17578  lbsextlem4  17590  psgnodpmr  18393  frlmsslsp  18596  frlmsslspOLD  18597  regsep2  19643  1stckgen  19790  regr1lem  19975  opnsubg  20341  zcld  21053  recld2  21054  bcthlem4  21501  iundisj  21693  iblss2  21947  itgeqa  21955  limcnlp  22017  dvloglem  22757  dvlog2lem  22761  ressatans  22993  wilthlem2  23071  tgelrnln  23724  tghilbert1_1  23731  nbcusgra  24139  usgrasscusgra  24159  uvtxnbgra  24169  frgrancvvdeqlem1  24707  frgrawopreglem4  24724  iundisjf  27121  iundisjfi  27269  elzrhunit  27596  qqhval2  27599  plymulx  28145  signstfvneq0  28169  regamcl  28243  facgam  28248  prodrblem  28638  fprodcvg  28639  fprodss  28657  onint1  29491  dvtanlem  29641  dvasin  29680  areacirclem4  29687  pridlc3  30073  rmspecsqrtnq  30446  rmspecnonsq  30447  climrec  31145  limcrecl  31171  sumnnodd  31172  lptioo2  31173  lptioo1  31174  reclimc  31195  fperdvper  31248  itgcoscmulx  31287  itgsincmulx  31292  stoweidlem34  31334  stoweidlem39  31339  stoweidlem57  31357  wallispi  31370  stirlinglem8  31381  dirkercncflem2  31404  dirkercncflem4  31406  fourierdlem38  31445  fourierdlem40  31447  fourierdlem42  31449  fourierdlem46  31453  fourierdlem53  31460  fourierdlem56  31463  fourierdlem58  31465  fourierdlem62  31469  fourierdlem74  31481  fourierdlem75  31482  fourierdlem76  31483  fourierdlem78  31485  fourierdlem93  31500  fouriersw  31532  usgra2pthlem1  31822