Theorem eldifad 3913

Description: If a class is in the difference of two classes, it is also in the minuend. One-way deduction form of eldif 3911. (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 3911	. . 3 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))
3	1, 2	sylib 218	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))
4	3	simpld 494	1 ⊢ (𝜑 → 𝐴 ∈ 𝐵)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904

This theorem is referenced by:  xpdifid  6126  fvdifsupp  8113  unblem1  9192  cantnflem3  9600  cantnflem4  9601  oef1o  9607  infxpenc  9928  acndom2  9964  ackbij1lem18  10146  infpssrlem3  10215  fin23lem26  10235  fin23lem30  10252  pwfseqlem4a  10572  elfzodif0  13686  expclz  14007  pfxchn  18533  chnind  18544  chnccats1  18548  chnccat  18549  symgextf  19346  pmtrfinv  19390  symggen  19399  efgsdmi  19661  efgs1b  19665  efgsp1  19666  efgsres  19667  efgredlemf  19670  efgredlemd  19673  efgredlemc  19674  efgredlem  19676  efgrelexlemb  19679  gsum2d2lem  19902  pgpfac1lem2  20006  pgpfac1lem3a  20007  pgpfac1lem3  20008  pgpfac1lem4  20009  zrzeroorngc  20577  zrtermoringc  20608  zrninitoringc  20609  domneq0r  20657  isdrng2  20676  fidomndrnglem  20705  lvecinv  21068  lspsncmp  21071  lspsnne1  21072  lspsnnecom  21074  lspabs2  21075  lspsneu  21078  lspdisjb  21081  lspexch  21084  lspindp1  21088  lvecindp2  21094  lspsolv  21098  lspsnat  21100  lsppratlem1  21102  lsppratlem2  21103  nzerooringczr  21435  frlmssuvc2  21750  evls1fpws  22313  maducoeval2  22584  hauscmplem  23350  1stccnp  23406  imasdsf1olem  24317  rrxmetlem  25363  divcncf  25404  dvrec  25915  dvmptdiv  25934  ftc1lem6  26004  elqaalem1  26283  elqaalem3  26285  ulmdvlem3  26367  abelthlem6  26402  abelthlem7a  26403  abelthlem7  26404  logtayl  26625  dmgmn0  26992  dmgmaddnn0  26993  dmgmdivn0  26994  lgamgulmlem2  26996  lgamgulmlem3  26997  lgamgulmlem5  26999  lgamgulmlem6  27000  lgamgulm2  27002  lgambdd  27003  lgamucov  27004  lgamcvg2  27021  gamcvg  27022  gamcvg2lem  27025  ftalem3  27041  lgsqrlem1  27313  lgsqrlem2  27314  lgsqrlem3  27315  lgsqrlem4  27316  lgseisenlem1  27342  lgseisenlem2  27343  lgseisenlem3  27344  lgseisenlem4  27345  lgseisen  27346  lgsquadlem1  27347  lgsquadlem2  27348  lgsquadlem3  27349  chebbnd1lem1  27436  dchrisum0re  27480  dchrisum0lema  27481  dchrisum0lem1b  27482  dchrisum0lem1  27483  dchrisum0lem2a  27484  dchrisum0lem2  27485  tgisline  28699  elntg  29057  uhgrss  29137  upgrex  29165  edguhgr  29202  1loopgrvd0  29578  disjiunel  32671  suppovss  32760  nn0difffzod  32884  gsumfs2d  33144  gsumhashmul  33150  odpmco  33168  pmtrcnel  33171  pmtrcnelor  33173  cycpmco2f1  33206  cycpmco2rn  33207  cycpmco2lem1  33208  cycpmco2lem2  33209  cycpmco2lem3  33210  cycpmco2lem4  33211  cycpmco2lem5  33212  cycpmco2lem6  33213  cycpmco2lem7  33214  cycpmco2  33215  cyc3co2  33222  tocyccntz  33226  cyc3conja  33239  fxpsdrg  33257  elrgspnlem2  33325  elrgspnlem4  33327  elrgspnsubrunlem2  33330  domnprodn0  33357  domnprodeq0  33358  idomrcanOLD  33364  isdrng4  33377  fracfld  33390  lindssn  33459  lindfpropd  33463  elrspunidl  33509  elrspunsn  33510  drngidl  33514  mxidlmaxv  33549  mxidlirredi  33552  opprqusdrng  33574  qsdrnglem2  33577  rprmcl  33599  rprmirred  33612  pidufd  33624  1arithufdlem3  33627  dfufd2  33631  zringfrac  33635  deg1prod  33664  ply1dg3rt0irred  33665  gsummoncoe1fzo  33678  mplvrpmrhm  33712  esplyfval2  33723  lindsunlem  33781  fedgmullem1  33786  fedgmullem2  33787  assafld  33794  fldextrspunlsp  33831  extdgfialglem2  33850  irngnminplynz  33869  constrextdg2lem  33905  constrfiss  33908  constrsdrg  33932  submatminr1  33967  qtophaus  33993  qqhval2  34139  esummono  34211  gsumesum  34216  esum2dlem  34249  measvuni  34371  fiunelcarsg  34473  sitgclg  34499  sitgaddlemb  34505  eulerpartlemsv2  34515  eulerpartlemsv3  34518  eulerpartlemgc  34519  eulerpartlemv  34521  signstfvneq0  34729  signstfvcl  34730  signstfveq0a  34733  signstfveq0  34734  signsvfn  34739  signsvtp  34740  signsvtn  34741  signsvfpn  34742  signsvfnn  34743  signlem0  34744  hgt750leme  34815  onvf1odlem4  35300  iprodgam  35936  poimirlem2  37823  rrndstprj2  38032  lsatelbN  39276  lsatfixedN  39279  lkreqN  39440  lkrlspeqN  39441  dochnel2  41662  dochnel  41663  djhcvat42  41685  dochsnshp  41723  dochexmidat  41729  dochsnkr  41742  dochsnkr2  41743  dochsnkr2cl  41744  dochflcl  41745  dochfl1  41746  dochfln0  41747  lcfl6lem  41768  lcfl7lem  41769  lcfl8b  41774  lclkrlem2a  41777  lclkrlem2b  41778  lclkrlem2c  41779  lclkrlem2d  41780  lclkrlem2e  41781  lclkrlem2f  41782  lcfrlem14  41826  lcfrlem15  41827  lcfrlem16  41828  lcfrlem17  41829  lcfrlem18  41830  lcfrlem19  41831  lcfrlem20  41832  lcfrlem21  41833  lcfrlem23  41835  lcfrlem25  41837  lcfrlem26  41838  lcfrlem35  41847  lcfrlem36  41848  mapdn0  41939  mapdpglem29  41970  mapdpglem24  41974  baerlem3lem1  41977  baerlem5alem1  41978  baerlem5blem1  41979  baerlem3lem2  41980  baerlem5alem2  41981  baerlem5blem2  41982  baerlem5amN  41986  baerlem5bmN  41987  baerlem5abmN  41988  mapdindp0  41989  mapdindp1  41990  mapdindp2  41991  mapdindp3  41992  mapdindp4  41993  mapdheq2  41999  mapdheq4lem  42001  mapdheq4  42002  mapdh6lem1N  42003  mapdh6lem2N  42004  mapdh6aN  42005  mapdh6bN  42007  mapdh6cN  42008  mapdh6dN  42009  mapdh6eN  42010  mapdh6fN  42011  mapdh6gN  42012  mapdh6hN  42013  mapdh6iN  42014  mapdh7eN  42018  mapdh7cN  42019  mapdh7dN  42020  mapdh7fN  42021  mapdh75e  42022  mapdh75fN  42025  hvmaplfl  42037  mapdhvmap  42039  mapdh8aa  42046  mapdh8ab  42047  mapdh8ad  42049  mapdh8b  42050  mapdh8c  42051  mapdh8d0N  42052  mapdh8d  42053  mapdh8e  42054  mapdh9a  42059  mapdh9aOLDN  42060  hdmap1val2  42070  hdmap1eq  42071  hdmap1valc  42073  hdmap1eq2  42075  hdmap1eq4N  42076  hdmap1l6lem1  42077  hdmap1l6lem2  42078  hdmap1l6a  42079  hdmap1l6b  42081  hdmap1l6c  42082  hdmap1l6d  42083  hdmap1l6e  42084  hdmap1l6f  42085  hdmap1l6g  42086  hdmap1l6h  42087  hdmap1l6i  42088  hdmap1eulem  42092  hdmap1eulemOLDN  42093  hdmapcl  42100  hdmapval2lem  42101  hdmapval0  42103  hdmapeveclem  42104  hdmapevec  42105  hdmapval3lemN  42107  hdmapval3N  42108  hdmap10lem  42109  hdmap11lem1  42111  hdmap11lem2  42112  hdmapnzcl  42115  hdmaprnlem3N  42120  hdmaprnlem3uN  42121  hdmaprnlem4N  42123  hdmaprnlem7N  42125  hdmaprnlem8N  42126  hdmaprnlem9N  42127  hdmaprnlem3eN  42128  hdmaprnlem16N  42132  hdmap14lem1  42138  hdmap14lem2N  42139  hdmap14lem3  42140  hdmap14lem4a  42141  hdmap14lem6  42143  hdmap14lem8  42145  hdmap14lem9  42146  hdmap14lem10  42147  hdmap14lem11  42148  hdmap14lem12  42149  hgmaprnlem1N  42166  hgmaprnlem2N  42167  hgmaprnlem3N  42168  hgmaprnlem4N  42169  hdmapip1  42186  hdmapinvlem1  42188  hdmapinvlem2  42189  hdmapinvlem3  42190  hdmapinvlem4  42191  hdmapglem5  42192  hgmapvvlem1  42193  hgmapvvlem2  42194  hgmapvvlem3  42195  hdmapglem7a  42197  hdmapglem7b  42198  hdmapglem7  42199  evl1gprodd  42381  nelsubginvcld  42761  nelsubgcld  42762  nelsubgsubcld  42763  domnexpgn0cl  42788  fidomncyc  42800  prjspnfv01  42877  prjspner01  42878  prjspner1  42879  dffltz  42887  qirropth  43160  rmxyneg  43172  rmxm1  43186  rmxluc  43188  rmxdbl  43191  ltrmxnn0  43201  jm2.19lem1  43241  jm2.23  43248  rmxdiophlem  43267  aomclem2  43307  cantnftermord  43572  inaex  44548  bccm1k  44593  dstregt0  45540  fprodexp  45850  fprodabs2  45851  mccllem  45853  fprodcnlem  45855  climrec  45859  climdivf  45868  islpcn  45893  lptre2pt  45894  0ellimcdiv  45903  reclimc  45907  divlimc  45910  cncficcgt0  46142  dvdivf  46176  stoweidlem34  46288  stoweidlem43  46297  etransclem46  46534  etransclem47  46535  etransclem48  46536  hsphoidmvle2  46839  hsphoidmvle  46840  hoidmvlelem3  46851  hoidmvlelem4  46852  hspdifhsp  46870  readdcnnred  47559  resubcnnred  47560  recnmulnred  47561  cndivrenred  47562