Theorem eldifd 3390

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

Syntax hints:   -. wn 3   -> wi 4   e. wcel 1872   \ cdif 3376

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-v 3024  df-dif 3382

This theorem is referenced by:  eqoreldif  3984  xpdifid  5227  ressuppssdif  6891  oaf1o  7219  findcard2d  7766  cantnflem1  8146  cantnflem2  8147  fin23lem26  8706  isf34lem4  8758  isfin7-2  8777  axdc3lem4  8834  axdc4lem  8836  ttukeylem7  8896  pwfseqlem1  9034  pwfseqlem3  9036  hashf1lem1  12566  seqcoll  12575  seqcoll2  12576  rlimcld2  13585  sumrblem  13720  fsumcvg  13721  fsumss  13734  incexclem  13837  prodrblem  13926  fprodcvg  13927  fprodss  13945  fprodn0f  13988  ruclem12  14236  coprmproddvdslem  14622  prmreclem5  14807  ramub1lem1  14927  mreexd  15491  frgpnabllem1  17452  gsumzaddlem  17497  gsum2d  17547  dmdprdsplitlem  17613  pgpfac1lem2  17651  pgpfac1lem3  17653  irredrmul  17878  lsppratlem3  18315  lbsextlem4  18327  psgnodpmr  19100  frlmsslsp  19296  regsep2  20334  1stckgen  20511  regr1lem  20696  opnsubg  21064  zcld  21773  recld2  21774  bcthlem4  22237  iundisj  22443  iblss2  22705  itgeqa  22713  limcnlp  22775  dvloglem  23535  dvlog2lem  23539  ressatans  23802  regamcl  23928  facgam  23933  wilthlem2  23936  tgelrnln  24617  nbcusgra  25133  usgrasscusgra  25153  uvtxnbgra  25163  frgrancvvdeqlem1  25700  frgrawopreglem4  25717  iundisjf  28145  iundisjfi  28322  submateqlem1  28585  submateqlem2  28586  elzrhunit  28735  qqhval2  28738  esumrnmpt2  28841  inelpisys  28928  carsgclctunlem1  29101  plymulx  29389  signstfvneq0  29413  onint1  31058  poimirlem23  31870  poimirlem30  31877  dvtanlemOLD  31898  dvasin  31935  areacirclem4  31942  pridlc3  32213  rmspecsqrtnq  35667  rmspecnonsq  35668  disjf1o  37370  icoiccdif  37517  climrec  37564  limciccioolb  37584  limcrecl  37592  sumnnodd  37593  lptioo2  37594  lptioo1  37595  limcicciooub  37600  lptre2pt  37603  reclimc  37617  icccncfext  37648  fperdvper  37673  dvnmul  37701  itgcoscmulx  37729  itgsincmulx  37734  stoweidlem34  37778  stoweidlem39  37783  stoweidlem57  37801  wallispi  37815  stirlinglem8  37826  dirkercncflem2  37849  dirkercncflem4  37851  fourierdlem38  37891  fourierdlem40  37893  fourierdlem42  37895  fourierdlem42OLD  37896  fourierdlem46  37899  fourierdlem53  37906  fourierdlem56  37909  fourierdlem58  37911  fourierdlem62  37915  fourierdlem74  37927  fourierdlem75  37928  fourierdlem76  37929  fourierdlem78  37931  fourierdlem93  37946  fourierdlem103  37956  fourierdlem104  37957  fouriersw  37978  elaa2  37982  etransc  38032  gsumge0cl  38064  sge0fodjrnlem  38109  iundjiun  38149  meadjiunlem  38154  caragendifcl  38186  caratheodorylem1  38198  hoidmvlelem1  38264  hoidmvlelem2  38265  hoidmvlelem4  38267  incistruhgr  38947  upgrres1  39127  usgra2pthlem1  39268  dig1  40022