Theorem eldifad 3586

Description: If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3584. (Contributed by David Moews, 1-May-2017.)

Hypothesis

Ref	Expression
eldifad.1	|- ( ph -> A e. ( B \ C ) )

Assertion

Ref	Expression
eldifad	|- ( ph -> A e. B )

Proof of Theorem eldifad

Step	Hyp	Ref	Expression
1		eldifad.1	. . 3 |- ( ph -> A e. ( B \ C ) )
2		eldif 3584	. . 3 |- ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )
3	1, 2	sylib 208	. 2 |- ( ph -> ( A e. B /\ -. A e. C ) )
4	3	simpld 475	1 |- ( ph -> A e. B )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 384   e. wcel 1990   \ cdif 3571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577

This theorem is referenced by:  xpdifid  5562  unblem1  8212  cantnflem3  8588  cantnflem4  8589  oef1o  8595  infxpenc  8841  acndom2  8877  ackbij1lem18  9059  infpssrlem3  9127  fin23lem26  9147  fin23lem30  9164  pwfseqlem4a  9483  expclz  12885  symgextf  17837  pmtrfinv  17881  symggen  17890  efgsdmi  18145  efgs1b  18149  efgsp1  18150  efgsres  18151  efgredlemf  18154  efgredlemd  18157  efgredlem  18160  efgrelexlemb  18163  gsum2d2lem  18372  pgpfac1lem2  18474  pgpfac1lem3a  18475  pgpfac1lem3  18476  pgpfac1lem4  18477  isdrng2  18757  lvecinv  19113  lspsncmp  19116  lspsnne1  19117  lspsnnecom  19119  lspabs2  19120  lspsneu  19123  lspdisjb  19126  lspexch  19129  lspindp1  19133  lvecindp2  19139  lspsolv  19143  lspsnat  19145  lsppratlem1  19147  lsppratlem2  19148  fidomndrnglem  19306  frlmssuvc2  20134  maducoeval2  20446  hauscmplem  21209  1stccnp  21265  imasdsf1olem  22178  rrxmetlem  23190  divcncf  23216  dvrec  23718  dvmptdiv  23737  ftc1lem6  23804  elqaalem1  24074  elqaalem3  24076  ulmdvlem3  24156  abelthlem6  24190  abelthlem7a  24191  abelthlem7  24192  logtayl  24406  dmgmn0  24752  dmgmaddnn0  24753  dmgmdivn0  24754  lgamgulmlem2  24756  lgamgulmlem3  24757  lgamgulmlem5  24759  lgamgulmlem6  24760  lgamgulm2  24762  lgambdd  24763  lgamucov  24764  lgamcvg2  24781  gamcvg  24782  gamcvg2lem  24785  ftalem3  24801  lgsqrlem1  25071  lgsqrlem2  25072  lgsqrlem3  25073  lgsqrlem4  25074  lgseisenlem1  25100  lgseisenlem2  25101  lgseisenlem3  25102  lgseisenlem4  25103  lgseisen  25104  lgsquadlem2  25106  lgsquadlem3  25107  chebbnd1lem1  25158  dchrisum0re  25202  dchrisum0lema  25203  dchrisum0lem1b  25204  dchrisum0lem1  25205  dchrisum0lem2a  25206  dchrisum0lem2  25207  tgisline  25522  elntg  25864  uhgrss  25959  upgrex  25987  edguhgr  26024  1loopgrvd0  26400  disjiunel  29409  submatminr1  29876  qtophaus  29903  qqhval2  30026  esummono  30116  gsumesum  30121  esum2dlem  30154  measvuni  30277  fiunelcarsg  30378  sitgclg  30404  sitgaddlemb  30410  eulerpartlemsv2  30420  eulerpartlemsv3  30423  eulerpartlemgc  30424  eulerpartlemv  30426  signstfvneq0  30649  signstfvcl  30650  signstfveq0a  30653  signstfveq0  30654  signsvfn  30659  signsvtp  30660  signsvtn  30661  signsvfpn  30662  signsvfnn  30663  signlem0  30664  hgt750leme  30736  iprodgam  31628  poimirlem2  33411  rrndstprj2  33630  lsatelbN  34293  lsatfixedN  34296  lkreqN  34457  lkrlspeqN  34458  dochnel2  36681  dochnel  36682  djhcvat42  36704  dochsnshp  36742  dochexmidat  36748  dochsnkr  36761  dochsnkr2  36762  dochsnkr2cl  36763  dochflcl  36764  dochfl1  36765  dochfln0  36766  lcfl6lem  36787  lcfl7lem  36788  lcfl8b  36793  lclkrlem2a  36796  lclkrlem2b  36797  lclkrlem2c  36798  lclkrlem2d  36799  lclkrlem2e  36800  lclkrlem2f  36801  lcfrlem14  36845  lcfrlem15  36846  lcfrlem16  36847  lcfrlem17  36848  lcfrlem18  36849  lcfrlem19  36850  lcfrlem20  36851  lcfrlem21  36852  lcfrlem23  36854  lcfrlem25  36856  lcfrlem26  36857  lcfrlem35  36866  lcfrlem36  36867  mapdn0  36958  mapdpglem29  36989  mapdpglem24  36993  baerlem3lem1  36996  baerlem5alem1  36997  baerlem5blem1  36998  baerlem3lem2  36999  baerlem5alem2  37000  baerlem5blem2  37001  baerlem5amN  37005  baerlem5bmN  37006  baerlem5abmN  37007  mapdindp0  37008  mapdindp1  37009  mapdindp2  37010  mapdindp3  37011  mapdindp4  37012  mapdheq2  37018  mapdheq4lem  37020  mapdheq4  37021  mapdh6lem1N  37022  mapdh6lem2N  37023  mapdh6aN  37024  mapdh6bN  37026  mapdh6cN  37027  mapdh6dN  37028  mapdh6eN  37029  mapdh6fN  37030  mapdh6gN  37031  mapdh6hN  37032  mapdh6iN  37033  mapdh7eN  37037  mapdh7cN  37038  mapdh7dN  37039  mapdh7fN  37040  mapdh75e  37041  mapdh75fN  37044  hvmaplfl  37056  mapdhvmap  37058  mapdh8aa  37065  mapdh8ab  37066  mapdh8ad  37068  mapdh8b  37069  mapdh8c  37070  mapdh8d0N  37071  mapdh8d  37072  mapdh8e  37073  mapdh9a  37079  mapdh9aOLDN  37080  hdmap1val2  37090  hdmap1eq  37091  hdmap1valc  37093  hdmap1eq2  37095  hdmap1eq4N  37096  hdmap1l6lem1  37097  hdmap1l6lem2  37098  hdmap1l6a  37099  hdmap1l6b  37101  hdmap1l6c  37102  hdmap1l6d  37103  hdmap1l6e  37104  hdmap1l6f  37105  hdmap1l6g  37106  hdmap1l6h  37107  hdmap1l6i  37108  hdmap1eulem  37113  hdmap1eulemOLDN  37114  hdmap1neglem1N  37117  hdmapcl  37122  hdmapval2lem  37123  hdmapval0  37125  hdmapeveclem  37126  hdmapevec  37127  hdmapval3lemN  37129  hdmapval3N  37130  hdmap10lem  37131  hdmap11lem1  37133  hdmap11lem2  37134  hdmapnzcl  37137  hdmaprnlem3N  37142  hdmaprnlem3uN  37143  hdmaprnlem4N  37145  hdmaprnlem7N  37147  hdmaprnlem8N  37148  hdmaprnlem9N  37149  hdmaprnlem3eN  37150  hdmaprnlem16N  37154  hdmap14lem1  37160  hdmap14lem2N  37161  hdmap14lem3  37162  hdmap14lem4a  37163  hdmap14lem6  37165  hdmap14lem8  37167  hdmap14lem9  37168  hdmap14lem10  37169  hdmap14lem11  37170  hdmap14lem12  37171  hgmaprnlem1N  37188  hgmaprnlem2N  37189  hgmaprnlem3N  37190  hgmaprnlem4N  37191  hdmapip1  37208  hdmapinvlem1  37210  hdmapinvlem2  37211  hdmapinvlem3  37212  hdmapinvlem4  37213  hdmapglem5  37214  hgmapvvlem1  37215  hgmapvvlem2  37216  hgmapvvlem3  37217  hdmapglem7a  37219  hdmapglem7b  37220  hdmapglem7  37221  qirropth  37473  rmxyneg  37485  rmxm1  37499  rmxluc  37501  rmxdbl  37504  ltrmxnn0  37516  jm2.19lem1  37556  jm2.23  37563  rmxdiophlem  37582  aomclem2  37625  bccm1k  38541  dstregt0  39493  fprodexp  39826  fprodabs2  39827  mccllem  39829  fprodcnlem  39831  climrec  39835  climdivf  39844  islpcn  39871  lptre2pt  39872  0ellimcdiv  39881  reclimc  39885  divlimc  39888  cncficcgt0  40101  dvdivf  40137  stoweidlem34  40251  stoweidlem43  40260  etransclem46  40497  etransclem47  40498  etransclem48  40499  hsphoidmvle2  40799  hsphoidmvle  40800  hoidmvlelem3  40811  hoidmvlelem4  40812  hspdifhsp  40830  zrzeroorngc  42002  zrtermoringc  42070  zrninitoringc  42071  nzerooringczr  42072