Theorem eldifd 3470

Description: If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif 3469. (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 3469	. 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 1802   \ cdif 3456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-v 3095  df-dif 3462

This theorem is referenced by:  xpdifid  5422  ressuppssdif  6920  oaf1o  7211  findcard2d  7761  cantnflem1  8108  cantnflem2  8109  cantnflem1OLD  8131  fin23lem26  8705  isf34lem4  8757  isfin7-2  8776  axdc3lem4  8833  axdc4lem  8835  ttukeylem7  8895  pwfseqlem1  9036  pwfseqlem3  9038  hashf1lem1  12480  seqcoll  12488  seqcoll2  12489  rlimcld2  13377  sumrblem  13509  fsumcvg  13510  fsumss  13523  incexclem  13624  ruclem12  13848  prmreclem5  14312  ramub1lem1  14418  mreexd  14913  frgpnabllem1  16748  gsumzaddlem  16805  gsumzaddlemOLD  16807  gsum2d  16870  gsum2dOLD  16871  dmdprdsplitlem  16955  dmdprdsplitlemOLD  16956  pgpfac1lem2  16997  pgpfac1lem3  16999  irredrmul  17227  lsppratlem3  17666  lbsextlem4  17678  psgnodpmr  18496  frlmsslsp  18699  frlmsslspOLD  18700  regsep2  19747  1stckgen  19925  regr1lem  20110  opnsubg  20476  zcld  21188  recld2  21189  bcthlem4  21636  iundisj  21828  iblss2  22082  itgeqa  22090  limcnlp  22152  dvloglem  22898  dvlog2lem  22902  ressatans  23134  wilthlem2  23212  tgelrnln  23879  nbcusgra  24332  usgrasscusgra  24352  uvtxnbgra  24362  frgrancvvdeqlem1  24899  frgrawopreglem4  24916  iundisjf  27317  iundisjfi  27470  elzrhunit  27830  qqhval2  27833  plymulx  28375  signstfvneq0  28399  regamcl  28473  facgam  28478  prodrblem  29033  fprodcvg  29034  fprodss  29052  onint1  29886  dvtanlem  30036  dvasin  30075  areacirclem4  30082  pridlc3  30442  rmspecsqrtnq  30814  rmspecnonsq  30815  icoiccdif  31500  climrec  31517  limciccioolb  31535  limcrecl  31543  sumnnodd  31544  lptioo2  31545  lptioo1  31546  limcicciooub  31551  lptre2pt  31554  reclimc  31567  icccncfext  31597  fperdvper  31619  itgcoscmulx  31658  itgsincmulx  31663  stoweidlem34  31705  stoweidlem39  31710  stoweidlem57  31728  wallispi  31741  stirlinglem8  31752  dirkercncflem2  31775  dirkercncflem4  31777  fourierdlem38  31816  fourierdlem40  31818  fourierdlem42  31820  fourierdlem46  31824  fourierdlem53  31831  fourierdlem56  31834  fourierdlem58  31836  fourierdlem62  31840  fourierdlem74  31852  fourierdlem75  31853  fourierdlem76  31854  fourierdlem78  31856  fourierdlem93  31871  fourierdlem103  31881  fourierdlem104  31882  fouriersw  31903  usgra2pthlem1  32191