Theorem eldifad 3911

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∈ wcel 2145   ∖ cdif 3896

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-dif 3902

This theorem is used by:  xpdifid  6159  xpdifcnvepel  6160  fvdifsupp  8188  unblem1  9284  cantnflem3  9692  cantnflem4  9693  oef1o  9699  infxpenc  10097  acndom2  10133  ackbij1lem18  10314  infpssrlem3  10383  fin23lem26  10403  fin23lem30  10420  pwfseqlem4a  10746  elfzodif0  13905  expclz  14227  pfxchn  18784  chnind  18795  chnccats1  18799  chnccat  18800  symgextf  19631  pmtrfinv  19675  symggen  19684  efgsdmi  19946  efgs1b  19950  efgsp1  19951  efgsres  19952  efgredlemf  19955  efgredlemd  19958  efgredlemc  19959  efgredlem  19961  efgrelexlemb  19964  gsum2d2lem  20187  pgpfac1lem2  20291  pgpfac1lem3a  20292  pgpfac1lem3  20293  pgpfac1lem4  20294  zrzeroorngc  20896  zrtermoringc  20927  zrninitoringc  20928  domneq0r  20975  isdrng4  20992  isdrng2  20997  fidomndrnglem  21030  lvecinv  21391  lspsncmp  21394  lspsnne1  21395  lspsnnecom  21397  lspabs2  21398  lspsneu  21401  lspdisjb  21404  lspexch  21407  lspindp1  21411  lvecindp2  21417  lspsolv  21421  lspsnat  21423  lsppratlem1  21425  lsppratlem2  21426  drngidl  21539  prmidlsubm  21643  nzerooringczr  21786  frlmssuvc2  22101  evls1fpws  22687  maducoeval2  22955  hauscmplem  23724  1stccnp  23781  imasdsf1olem  24692  rrxmetlem  25728  divcncf  25768  dvrec  26275  dvmptdiv  26294  ftc1lem6  26361  elqaalem1  26642  elqaalem3  26644  ulmdvlem3  26729  abelthlem6  26763  abelthlem7a  26764  abelthlem7  26765  logtayl  26988  dmgmn0  27353  dmgmaddnn0  27354  dmgmdivn0  27355  lgamgulmlem2  27357  lgamgulmlem3  27358  lgamgulmlem5  27360  lgamgulmlem6  27361  lgamgulm2  27363  lgambdd  27364  lgamucov  27365  lgamcvg2  27382  gamcvg  27383  gamcvg2lem  27386  ftalem3  27402  lgsqrlem1  27673  lgsqrlem2  27674  lgsqrlem3  27675  lgsqrlem4  27676  lgseisenlem1  27702  lgseisenlem2  27703  lgseisenlem3  27704  lgseisenlem4  27705  lgseisen  27706  lgsquadlem1  27707  lgsquadlem2  27708  lgsquadlem3  27709  chebbnd1lem1  27796  dchrisum0re  27840  dchrisum0lema  27841  dchrisum0lem1b  27842  dchrisum0lem1  27843  dchrisum0lem2a  27844  dchrisum0lem2  27845  tgisline  29095  oppmir  29232  tgelrnpln  29254  elplng  29258  elplngid  29260  plngcplem  29263  plngrotlem1  29265  plngrotlem2  29266  plngrotlem3  29267  plngrot  29268  lnssplnglem  29269  lnssplng  29270  plngmiropp  29272  nhpmirhp  29276  ragsupplcgra  29345  perpeqlem  29347  angmgmaddlid  29392  angmgmaddrid  29393  angmgmlem  29395  dfprlng2  29425  perpprlng  29428  prlngex  29429  prlngmolem1  29430  prlngmolem2  29431  prlngeu  29433  prlngmid2  29439  elntg  29562  uhgrss  29642  upgrex  29670  edguhgr  29707  1loopgrvd0  30085  disjiunel  33190  suppovss  33274  nn0difffzod  33396  gsumfs2d  33622  gsumhashmul  33628  suppgsumssiun  33633  odpmco  33647  pmtrcnel  33650  pmtrcnelor  33652  cycpmco2f1  33685  cycpmco2rn  33686  cycpmco2lem1  33687  cycpmco2lem2  33688  cycpmco2lem3  33689  cycpmco2lem4  33690  cycpmco2lem5  33691  cycpmco2lem6  33692  cycpmco2lem7  33693  cycpmco2  33694  cyc3co2  33701  tocyccntz  33705  cyc3conja  33718  fxpsdrg  33736  elrgspnlem2  33804  elrgspnlem4  33806  elrgspnsubrunlem2  33809  domnprodn0  33839  domnprodeq0  33840  fracfld  33870  lindssn  33933  lindfpropd  33937  elrspunidl  33978  elrspunsn  33979  mxidlmaxv  33993  mxidlirredi  33996  opprqusdrng  34017  qsdrnglem2  34020  dflringlem  34026  dflringlem2  34027  rprmcl  34050  rprmirred  34063  pidufd  34075  1arithufdlem3  34078  dfufd2  34082  zringfrac  34086  deg1prod  34115  ply1dg3rt0irred  34116  gsummoncoe1fzo  34129  mplvrpmrhm  34179  psrgsum  34180  psrmonprod  34184  esplyfval2  34197  lindsunlem  34256  fedgmullem1  34261  fedgmullem2  34262  assafld  34269  fldextrspunlsp  34306  extdgfialglem2  34325  irngnminplynz  34344  constrextdg2lem  34380  constrfiss  34383  constrsdrg  34407  submatminr1  34442  qtophaus  34468  qqhval2  34614  esummono  34686  gsumesum  34691  esum2dlem  34724  measvuni  34847  fiunelcarsg  34948  sitgclg  34974  sitgaddlemb  34980  eulerpartlemsv2  34990  eulerpartlemsv3  34993  eulerpartlemgc  34994  eulerpartlemv  34996  signstfvneq0  35201  signstfvcl  35202  signstfveq0a  35205  signstfveq0  35206  signsvfn  35211  signsvtp  35212  signsvtn  35213  signsvfpn  35214  signsvfnn  35215  signlem0  35216  hgt750leme  35287  onvf1odlem4  35885  iprodgam  36507  ttcwf2  37313  mh-inf3f1  37329  poimirlem2  38540  rrndstprj2  38765  lsatelbN  40063  lsatfixedN  40066  lkreqN  40227  lkrlspeqN  40228  dochnel2  42449  dochnel  42450  djhcvat42  42472  dochsnshp  42510  dochexmidat  42516  dochsnkr  42529  dochsnkr2  42530  dochsnkr2cl  42531  dochflcl  42532  dochfl1  42533  dochfln0  42534  lcfl6lem  42555  lcfl7lem  42556  lcfl8b  42561  lclkrlem2a  42564  lclkrlem2b  42565  lclkrlem2c  42566  lclkrlem2d  42567  lclkrlem2e  42568  lclkrlem2f  42569  lcfrlem14  42613  lcfrlem15  42614  lcfrlem16  42615  lcfrlem17  42616  lcfrlem18  42617  lcfrlem19  42618  lcfrlem20  42619  lcfrlem21  42620  lcfrlem23  42622  lcfrlem25  42624  lcfrlem26  42625  lcfrlem35  42634  lcfrlem36  42635  mapdn0  42726  mapdpglem29  42757  mapdpglem24  42761  baerlem3lem1  42764  baerlem5alem1  42765  baerlem5blem1  42766  baerlem3lem2  42767  baerlem5alem2  42768  baerlem5blem2  42769  baerlem5amN  42773  baerlem5bmN  42774  baerlem5abmN  42775  mapdindp0  42776  mapdindp1  42777  mapdindp2  42778  mapdindp3  42779  mapdindp4  42780  mapdheq2  42786  mapdheq4lem  42788  mapdheq4  42789  mapdh6lem1N  42790  mapdh6lem2N  42791  mapdh6aN  42792  mapdh6bN  42794  mapdh6cN  42795  mapdh6dN  42796  mapdh6eN  42797  mapdh6fN  42798  mapdh6gN  42799  mapdh6hN  42800  mapdh6iN  42801  mapdh7eN  42805  mapdh7cN  42806  mapdh7dN  42807  mapdh7fN  42808  mapdh75e  42809  mapdh75fN  42812  hvmaplfl  42824  mapdhvmap  42826  mapdh8aa  42833  mapdh8ab  42834  mapdh8ad  42836  mapdh8b  42837  mapdh8c  42838  mapdh8d0N  42839  mapdh8d  42840  mapdh8e  42841  mapdh9a  42846  mapdh9aOLDN  42847  hdmap1val2  42857  hdmap1eq  42858  hdmap1valc  42860  hdmap1eq2  42862  hdmap1eq4N  42863  hdmap1l6lem1  42864  hdmap1l6lem2  42865  hdmap1l6a  42866  hdmap1l6b  42868  hdmap1l6c  42869  hdmap1l6d  42870  hdmap1l6e  42871  hdmap1l6f  42872  hdmap1l6g  42873  hdmap1l6h  42874  hdmap1l6i  42875  hdmap1eulem  42879  hdmap1eulemOLDN  42880  hdmapcl  42887  hdmapval2lem  42888  hdmapval0  42890  hdmapeveclem  42891  hdmapevec  42892  hdmapval3lemN  42894  hdmapval3N  42895  hdmap10lem  42896  hdmap11lem1  42898  hdmap11lem2  42899  hdmapnzcl  42902  hdmaprnlem3N  42907  hdmaprnlem3uN  42908  hdmaprnlem4N  42910  hdmaprnlem7N  42912  hdmaprnlem8N  42913  hdmaprnlem9N  42914  hdmaprnlem3eN  42915  hdmaprnlem16N  42919  hdmap14lem1  42925  hdmap14lem2N  42926  hdmap14lem3  42927  hdmap14lem4a  42928  hdmap14lem6  42930  hdmap14lem8  42932  hdmap14lem9  42933  hdmap14lem10  42934  hdmap14lem11  42935  hdmap14lem12  42936  hgmaprnlem1N  42953  hgmaprnlem2N  42954  hgmaprnlem3N  42955  hgmaprnlem4N  42956  hdmapip1  42973  hdmapinvlem1  42975  hdmapinvlem2  42976  hdmapinvlem3  42977  hdmapinvlem4  42978  hdmapglem5  42979  hgmapvvlem1  42980  hgmapvvlem2  42981  hgmapvvlem3  42982  hdmapglem7a  42984  hdmapglem7b  42985  hdmapglem7  42986  evl1gprodd  43167  nelsubginvcld  43560  nelsubgcld  43561  nelsubgsubcld  43562  domnexpgn0cl  43584  fidomncyc  43599  frlmnzcoordex  43652  frlmnzcoordsca  43658  dffltz  43670  qirropth  43914  rmxyneg  43926  rmxm1  43940  rmxluc  43942  rmxdbl  43945  ltrmxnn0  43955  jm2.19lem1  43995  jm2.23  44002  rmxdiophlem  44021  aomclem2  44056  cantnftermord  44321  inaex  45280  bccm1k  45325  dstregt0  46297  fprodexp  46605  fprodabs2  46606  mccllem  46608  fprodcnlem  46610  climrec  46614  climdivf  46623  islpcn  46648  lptre2pt  46649  0ellimcdiv  46658  reclimc  46662  divlimc  46665  cncficcgt0  46897  dvdivf  46931  stoweidlem34  47043  stoweidlem43  47052  etransclem46  47289  etransclem47  47290  etransclem48  47291  hsphoidmvle2  47594  hsphoidmvle  47595  hoidmvlelem3  47606  hoidmvlelem4  47607  hspdifhsp  47625  readdcnnred  48372  resubcnnred  48373  recnmulnred  48374  cndivrenred  48375