Theorem eldifad 3915

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

Hypothesis

Ref	Expression
eldifad.1	⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶))

Assertion

Ref	Expression
eldifad	⊢ (𝜑 → 𝐴 ∈ 𝐵)

Proof of Theorem eldifad

Step	Hyp	Ref	Expression
1		eldifad.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ (𝐵 ∖ 𝐶))
2		eldif 3913	. . 3 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))
3	1, 2	sylib 218	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))
4	3	simpld 494	1 ⊢ (𝜑 → 𝐴 ∈ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2114   ∖ cdif 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-dif 3906

This theorem is referenced by:  xpdifid  6134  fvdifsupp  8123  unblem1  9204  cantnflem3  9612  cantnflem4  9613  oef1o  9619  infxpenc  9940  acndom2  9976  ackbij1lem18  10158  infpssrlem3  10227  fin23lem26  10247  fin23lem30  10264  pwfseqlem4a  10584  elfzodif0  13698  expclz  14019  pfxchn  18545  chnind  18556  chnccats1  18560  chnccat  18561  symgextf  19361  pmtrfinv  19405  symggen  19414  efgsdmi  19676  efgs1b  19680  efgsp1  19681  efgsres  19682  efgredlemf  19685  efgredlemd  19688  efgredlemc  19689  efgredlem  19691  efgrelexlemb  19694  gsum2d2lem  19917  pgpfac1lem2  20021  pgpfac1lem3a  20022  pgpfac1lem3  20023  pgpfac1lem4  20024  zrzeroorngc  20592  zrtermoringc  20623  zrninitoringc  20624  domneq0r  20672  isdrng2  20691  fidomndrnglem  20720  lvecinv  21083  lspsncmp  21086  lspsnne1  21087  lspsnnecom  21089  lspabs2  21090  lspsneu  21093  lspdisjb  21096  lspexch  21099  lspindp1  21103  lvecindp2  21109  lspsolv  21113  lspsnat  21115  lsppratlem1  21117  lsppratlem2  21118  nzerooringczr  21450  frlmssuvc2  21765  evls1fpws  22328  maducoeval2  22599  hauscmplem  23365  1stccnp  23421  imasdsf1olem  24332  rrxmetlem  25378  divcncf  25419  dvrec  25930  dvmptdiv  25949  ftc1lem6  26019  elqaalem1  26298  elqaalem3  26300  ulmdvlem3  26382  abelthlem6  26417  abelthlem7a  26418  abelthlem7  26419  logtayl  26640  dmgmn0  27007  dmgmaddnn0  27008  dmgmdivn0  27009  lgamgulmlem2  27011  lgamgulmlem3  27012  lgamgulmlem5  27014  lgamgulmlem6  27015  lgamgulm2  27017  lgambdd  27018  lgamucov  27019  lgamcvg2  27036  gamcvg  27037  gamcvg2lem  27040  ftalem3  27056  lgsqrlem1  27328  lgsqrlem2  27329  lgsqrlem3  27330  lgsqrlem4  27331  lgseisenlem1  27357  lgseisenlem2  27358  lgseisenlem3  27359  lgseisenlem4  27360  lgseisen  27361  lgsquadlem1  27362  lgsquadlem2  27363  lgsquadlem3  27364  chebbnd1lem1  27451  dchrisum0re  27495  dchrisum0lema  27496  dchrisum0lem1b  27497  dchrisum0lem1  27498  dchrisum0lem2a  27499  dchrisum0lem2  27500  tgisline  28715  elntg  29073  uhgrss  29153  upgrex  29181  edguhgr  29218  1loopgrvd0  29594  disjiunel  32687  suppovss  32775  nn0difffzod  32899  gsumfs2d  33159  gsumhashmul  33165  suppgsumssiun  33170  odpmco  33184  pmtrcnel  33187  pmtrcnelor  33189  cycpmco2f1  33222  cycpmco2rn  33223  cycpmco2lem1  33224  cycpmco2lem2  33225  cycpmco2lem3  33226  cycpmco2lem4  33227  cycpmco2lem5  33228  cycpmco2lem6  33229  cycpmco2lem7  33230  cycpmco2  33231  cyc3co2  33238  tocyccntz  33242  cyc3conja  33255  fxpsdrg  33273  elrgspnlem2  33341  elrgspnlem4  33343  elrgspnsubrunlem2  33346  domnprodn0  33373  domnprodeq0  33374  idomrcanOLD  33380  isdrng4  33393  fracfld  33406  lindssn  33475  lindfpropd  33479  elrspunidl  33525  elrspunsn  33526  drngidl  33530  mxidlmaxv  33565  mxidlirredi  33568  opprqusdrng  33590  qsdrnglem2  33593  rprmcl  33615  rprmirred  33628  pidufd  33640  1arithufdlem3  33643  dfufd2  33647  zringfrac  33651  deg1prod  33680  ply1dg3rt0irred  33681  gsummoncoe1fzo  33694  mplvrpmrhm  33728  psrgsum  33729  psrmonprod  33733  esplyfval2  33746  lindsunlem  33806  fedgmullem1  33811  fedgmullem2  33812  assafld  33819  fldextrspunlsp  33856  extdgfialglem2  33875  irngnminplynz  33894  constrextdg2lem  33930  constrfiss  33933  constrsdrg  33957  submatminr1  33992  qtophaus  34018  qqhval2  34164  esummono  34236  gsumesum  34241  esum2dlem  34274  measvuni  34396  fiunelcarsg  34498  sitgclg  34524  sitgaddlemb  34530  eulerpartlemsv2  34540  eulerpartlemsv3  34543  eulerpartlemgc  34544  eulerpartlemv  34546  signstfvneq0  34754  signstfvcl  34755  signstfveq0a  34758  signstfveq0  34759  signsvfn  34764  signsvtp  34765  signsvtn  34766  signsvfpn  34767  signsvfnn  34768  signlem0  34769  hgt750leme  34840  onvf1odlem4  35326  iprodgam  35962  poimirlem2  37877  rrndstprj2  38086  lsatelbN  39386  lsatfixedN  39389  lkreqN  39550  lkrlspeqN  39551  dochnel2  41772  dochnel  41773  djhcvat42  41795  dochsnshp  41833  dochexmidat  41839  dochsnkr  41852  dochsnkr2  41853  dochsnkr2cl  41854  dochflcl  41855  dochfl1  41856  dochfln0  41857  lcfl6lem  41878  lcfl7lem  41879  lcfl8b  41884  lclkrlem2a  41887  lclkrlem2b  41888  lclkrlem2c  41889  lclkrlem2d  41890  lclkrlem2e  41891  lclkrlem2f  41892  lcfrlem14  41936  lcfrlem15  41937  lcfrlem16  41938  lcfrlem17  41939  lcfrlem18  41940  lcfrlem19  41941  lcfrlem20  41942  lcfrlem21  41943  lcfrlem23  41945  lcfrlem25  41947  lcfrlem26  41948  lcfrlem35  41957  lcfrlem36  41958  mapdn0  42049  mapdpglem29  42080  mapdpglem24  42084  baerlem3lem1  42087  baerlem5alem1  42088  baerlem5blem1  42089  baerlem3lem2  42090  baerlem5alem2  42091  baerlem5blem2  42092  baerlem5amN  42096  baerlem5bmN  42097  baerlem5abmN  42098  mapdindp0  42099  mapdindp1  42100  mapdindp2  42101  mapdindp3  42102  mapdindp4  42103  mapdheq2  42109  mapdheq4lem  42111  mapdheq4  42112  mapdh6lem1N  42113  mapdh6lem2N  42114  mapdh6aN  42115  mapdh6bN  42117  mapdh6cN  42118  mapdh6dN  42119  mapdh6eN  42120  mapdh6fN  42121  mapdh6gN  42122  mapdh6hN  42123  mapdh6iN  42124  mapdh7eN  42128  mapdh7cN  42129  mapdh7dN  42130  mapdh7fN  42131  mapdh75e  42132  mapdh75fN  42135  hvmaplfl  42147  mapdhvmap  42149  mapdh8aa  42156  mapdh8ab  42157  mapdh8ad  42159  mapdh8b  42160  mapdh8c  42161  mapdh8d0N  42162  mapdh8d  42163  mapdh8e  42164  mapdh9a  42169  mapdh9aOLDN  42170  hdmap1val2  42180  hdmap1eq  42181  hdmap1valc  42183  hdmap1eq2  42185  hdmap1eq4N  42186  hdmap1l6lem1  42187  hdmap1l6lem2  42188  hdmap1l6a  42189  hdmap1l6b  42191  hdmap1l6c  42192  hdmap1l6d  42193  hdmap1l6e  42194  hdmap1l6f  42195  hdmap1l6g  42196  hdmap1l6h  42197  hdmap1l6i  42198  hdmap1eulem  42202  hdmap1eulemOLDN  42203  hdmapcl  42210  hdmapval2lem  42211  hdmapval0  42213  hdmapeveclem  42214  hdmapevec  42215  hdmapval3lemN  42217  hdmapval3N  42218  hdmap10lem  42219  hdmap11lem1  42221  hdmap11lem2  42222  hdmapnzcl  42225  hdmaprnlem3N  42230  hdmaprnlem3uN  42231  hdmaprnlem4N  42233  hdmaprnlem7N  42235  hdmaprnlem8N  42236  hdmaprnlem9N  42237  hdmaprnlem3eN  42238  hdmaprnlem16N  42242  hdmap14lem1  42248  hdmap14lem2N  42249  hdmap14lem3  42250  hdmap14lem4a  42251  hdmap14lem6  42253  hdmap14lem8  42255  hdmap14lem9  42256  hdmap14lem10  42257  hdmap14lem11  42258  hdmap14lem12  42259  hgmaprnlem1N  42276  hgmaprnlem2N  42277  hgmaprnlem3N  42278  hgmaprnlem4N  42279  hdmapip1  42296  hdmapinvlem1  42298  hdmapinvlem2  42299  hdmapinvlem3  42300  hdmapinvlem4  42301  hdmapglem5  42302  hgmapvvlem1  42303  hgmapvvlem2  42304  hgmapvvlem3  42305  hdmapglem7a  42307  hdmapglem7b  42308  hdmapglem7  42309  evl1gprodd  42491  nelsubginvcld  42870  nelsubgcld  42871  nelsubgsubcld  42872  domnexpgn0cl  42897  fidomncyc  42909  prjspnfv01  42986  prjspner01  42987  prjspner1  42988  dffltz  42996  qirropth  43269  rmxyneg  43281  rmxm1  43295  rmxluc  43297  rmxdbl  43300  ltrmxnn0  43310  jm2.19lem1  43350  jm2.23  43357  rmxdiophlem  43376  aomclem2  43416  cantnftermord  43681  inaex  44657  bccm1k  44702  dstregt0  45648  fprodexp  45958  fprodabs2  45959  mccllem  45961  fprodcnlem  45963  climrec  45967  climdivf  45976  islpcn  46001  lptre2pt  46002  0ellimcdiv  46011  reclimc  46015  divlimc  46018  cncficcgt0  46250  dvdivf  46284  stoweidlem34  46396  stoweidlem43  46405  etransclem46  46642  etransclem47  46643  etransclem48  46644  hsphoidmvle2  46947  hsphoidmvle  46948  hoidmvlelem3  46959  hoidmvlelem4  46960  hspdifhsp  46978  readdcnnred  47667  resubcnnred  47668  recnmulnred  47669  cndivrenred  47670