Theorem eldifd 3427

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

Syntax hints:   -. wn 3   -> wi 4   e. wcel 1898   \ cdif 3413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-dif 3419

This theorem is referenced by:  eqoreldif  4025  xpdifid  5284  ressuppssdif  6963  oaf1o  7290  findcard2d  7839  cantnflem1  8220  cantnflem2  8221  fin23lem26  8781  isf34lem4  8833  isfin7-2  8852  axdc3lem4  8909  axdc4lem  8911  ttukeylem7  8971  pwfseqlem1  9109  pwfseqlem3  9111  hashf1lem1  12651  seqcoll  12660  seqcoll2  12661  rlimcld2  13691  sumrblem  13826  fsumcvg  13827  fsumss  13840  incexclem  13943  prodrblem  14032  fprodcvg  14033  fprodss  14051  fprodn0f  14094  ruclem12  14342  coprmproddvdslem  14728  prmreclem5  14913  ramub1lem1  15033  mreexd  15597  frgpnabllem1  17558  gsumzaddlem  17603  gsum2d  17653  dmdprdsplitlem  17719  pgpfac1lem2  17757  pgpfac1lem3  17759  irredrmul  17984  lsppratlem3  18421  lbsextlem4  18433  psgnodpmr  19207  frlmsslsp  19403  regsep2  20441  1stckgen  20618  regr1lem  20803  opnsubg  21171  zcld  21880  recld2  21881  bcthlem4  22344  iundisj  22550  iblss2  22812  itgeqa  22820  limcnlp  22882  dvloglem  23642  dvlog2lem  23646  ressatans  23909  regamcl  24035  facgam  24040  wilthlem2  24043  tgelrnln  24724  nbcusgra  25240  usgrasscusgra  25260  uvtxnbgra  25270  frgrancvvdeqlem1  25807  frgrawopreglem4  25824  iundisjf  28248  iundisjfi  28421  submateqlem1  28682  submateqlem2  28683  elzrhunit  28832  qqhval2  28835  esumrnmpt2  28938  inelpisys  29025  carsgclctunlem1  29198  plymulx  29486  signstfvneq0  29510  onint1  31158  poimirlem23  32008  poimirlem30  32015  dvtanlemOLD  32036  dvasin  32073  areacirclem4  32080  pridlc3  32351  rmspecsqrtnq  35799  rmspecnonsq  35800  disjf1o  37504  icoiccdif  37663  iccdificc  37679  climrec  37719  limciccioolb  37739  limcrecl  37747  sumnnodd  37748  lptioo2  37749  lptioo1  37750  limcicciooub  37755  lptre2pt  37758  reclimc  37772  icccncfext  37803  fperdvper  37828  dvnmul  37856  itgcoscmulx  37884  itgsincmulx  37889  stoweidlem34  37933  stoweidlem39  37938  stoweidlem57  37956  wallispi  37970  stirlinglem8  37981  dirkercncflem2  38004  dirkercncflem4  38006  fourierdlem38  38046  fourierdlem40  38048  fourierdlem42  38050  fourierdlem42OLD  38051  fourierdlem46  38054  fourierdlem53  38061  fourierdlem56  38064  fourierdlem58  38066  fourierdlem62  38070  fourierdlem74  38082  fourierdlem75  38083  fourierdlem76  38084  fourierdlem78  38086  fourierdlem93  38101  fourierdlem103  38111  fourierdlem104  38112  fouriersw  38133  elaa2  38137  etransc  38187  gsumge0cl  38251  sge0fodjrnlem  38296  iundjiun  38336  meadjiunlem  38341  caragendifcl  38373  caratheodorylem1  38385  hoidmvlelem1  38455  hoidmvlelem2  38456  hoidmvlelem4  38458  hspdifhsp  38476  hspmbllem2  38487  incistruhgr  39218  upgrres1  39430  usgra2pthlem1  39940  dig1  40692