Theorem eldifad 3925

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   ∈ wcel 2149   ∖ cdif 3910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-dif 3916

This theorem is referenced by:  xpdifid  6166  xpdifcnvepel  6167  fvdifsupp  8167  unblem1  9252  cantnflem3  9660  cantnflem4  9661  oef1o  9667  infxpenc  10002  acndom2  10038  ackbij1lem18  10219  infpssrlem3  10289  fin23lem26  10309  fin23lem30  10326  pwfseqlem4a  10646  elfzodif0  13799  expclz  14120  pfxchn  18666  chnind  18677  chnccats1  18681  chnccat  18682  symgextf  19487  pmtrfinv  19531  symggen  19540  efgsdmi  19802  efgs1b  19806  efgsp1  19807  efgsres  19808  efgredlemf  19811  efgredlemd  19814  efgredlemc  19815  efgredlem  19817  efgrelexlemb  19820  gsum2d2lem  20043  pgpfac1lem2  20147  pgpfac1lem3a  20148  pgpfac1lem3  20149  pgpfac1lem4  20150  zrzeroorngc  20729  zrtermoringc  20760  zrninitoringc  20761  domneq0r  20808  isdrng2  20827  fidomndrnglem  20854  lvecinv  21215  lspsncmp  21218  lspsnne1  21219  lspsnnecom  21221  lspabs2  21222  lspsneu  21225  lspdisjb  21228  lspexch  21231  lspindp1  21235  lvecindp2  21241  lspsolv  21245  lspsnat  21247  lsppratlem1  21249  lsppratlem2  21250  prmidlsubm  21456  nzerooringczr  21599  frlmssuvc2  21914  evls1fpws  22498  maducoeval2  22766  hauscmplem  23532  1stccnp  23588  imasdsf1olem  24499  rrxmetlem  25535  divcncf  25575  dvrec  26083  dvmptdiv  26102  ftc1lem6  26169  elqaalem1  26449  elqaalem3  26451  ulmdvlem3  26531  abelthlem6  26565  abelthlem7a  26566  abelthlem7  26567  logtayl  26791  dmgmn0  27156  dmgmaddnn0  27157  dmgmdivn0  27158  lgamgulmlem2  27160  lgamgulmlem3  27161  lgamgulmlem5  27163  lgamgulmlem6  27164  lgamgulm2  27166  lgambdd  27167  lgamucov  27168  lgamcvg2  27185  gamcvg  27186  gamcvg2lem  27189  ftalem3  27205  lgsqrlem1  27476  lgsqrlem2  27477  lgsqrlem3  27478  lgsqrlem4  27479  lgseisenlem1  27505  lgseisenlem2  27506  lgseisenlem3  27507  lgseisenlem4  27508  lgseisen  27509  lgsquadlem1  27510  lgsquadlem2  27511  lgsquadlem3  27512  chebbnd1lem1  27599  dchrisum0re  27643  dchrisum0lema  27644  dchrisum0lem1b  27645  dchrisum0lem1  27646  dchrisum0lem2a  27647  dchrisum0lem2  27648  tgisline  28862  oppmir  28995  tgelrnpln  29016  elplng  29020  elplngid  29022  plngcplem  29025  plngrotlem1  29027  plngrotlem2  29028  plngrotlem3  29029  plngrot  29030  lnssplnglem  29031  lnssplng  29032  plngmiropp  29034  nhpmirhp  29038  perpeqlem  29105  perpprlng  29153  prlngex  29154  prlngmolem1  29155  prlngmolem2  29156  prlngeu  29158  elntg  29275  uhgrss  29355  upgrex  29383  edguhgr  29420  1loopgrvd0  29795  disjiunel  32882  suppovss  32967  nn0difffzod  33090  gsumfs2d  33322  gsumhashmul  33328  suppgsumssiun  33333  odpmco  33347  pmtrcnel  33350  pmtrcnelor  33352  cycpmco2f1  33385  cycpmco2rn  33386  cycpmco2lem1  33387  cycpmco2lem2  33388  cycpmco2lem3  33389  cycpmco2lem4  33390  cycpmco2lem5  33391  cycpmco2lem6  33392  cycpmco2lem7  33393  cycpmco2  33394  cyc3co2  33401  tocyccntz  33405  cyc3conja  33418  fxpsdrg  33436  elrgspnlem2  33504  elrgspnlem4  33506  elrgspnsubrunlem2  33509  domnprodn0  33539  domnprodeq0  33540  isdrng4  33559  fracfld  33572  lindssn  33635  lindfpropd  33639  elrspunidl  33680  elrspunsn  33681  drngidl  33685  mxidlmaxv  33696  mxidlirredi  33699  opprqusdrng  33720  qsdrnglem2  33723  dflringlem  33729  dflringlem2  33730  rprmcl  33753  rprmirred  33766  pidufd  33778  1arithufdlem3  33781  dfufd2  33785  zringfrac  33789  deg1prod  33818  ply1dg3rt0irred  33819  gsummoncoe1fzo  33832  mplvrpmrhm  33882  psrgsum  33883  psrmonprod  33887  esplyfval2  33900  lindsunlem  33959  fedgmullem1  33964  fedgmullem2  33965  assafld  33972  fldextrspunlsp  34009  extdgfialglem2  34028  irngnminplynz  34047  constrextdg2lem  34083  constrfiss  34086  constrsdrg  34110  submatminr1  34145  qtophaus  34171  qqhval2  34317  esummono  34389  gsumesum  34394  esum2dlem  34427  measvuni  34549  fiunelcarsg  34651  sitgclg  34677  sitgaddlemb  34683  eulerpartlemsv2  34693  eulerpartlemsv3  34696  eulerpartlemgc  34697  eulerpartlemv  34699  signstfvneq0  34904  signstfvcl  34905  signstfveq0a  34908  signstfveq0  34909  signsvfn  34914  signsvtp  34915  signsvtn  34916  signsvfpn  34917  signsvfnn  34918  signlem0  34919  hgt750leme  34990  onvf1odlem4  35523  iprodgam  36167  ttcwf2  36959  mh-inf3f1  36975  poimirlem2  38195  rrndstprj2  38404  lsatelbN  39704  lsatfixedN  39707  lkreqN  39868  lkrlspeqN  39869  dochnel2  42090  dochnel  42091  djhcvat42  42113  dochsnshp  42151  dochexmidat  42157  dochsnkr  42170  dochsnkr2  42171  dochsnkr2cl  42172  dochflcl  42173  dochfl1  42174  dochfln0  42175  lcfl6lem  42196  lcfl7lem  42197  lcfl8b  42202  lclkrlem2a  42205  lclkrlem2b  42206  lclkrlem2c  42207  lclkrlem2d  42208  lclkrlem2e  42209  lclkrlem2f  42210  lcfrlem14  42254  lcfrlem15  42255  lcfrlem16  42256  lcfrlem17  42257  lcfrlem18  42258  lcfrlem19  42259  lcfrlem20  42260  lcfrlem21  42261  lcfrlem23  42263  lcfrlem25  42265  lcfrlem26  42266  lcfrlem35  42275  lcfrlem36  42276  mapdn0  42367  mapdpglem29  42398  mapdpglem24  42402  baerlem3lem1  42405  baerlem5alem1  42406  baerlem5blem1  42407  baerlem3lem2  42408  baerlem5alem2  42409  baerlem5blem2  42410  baerlem5amN  42414  baerlem5bmN  42415  baerlem5abmN  42416  mapdindp0  42417  mapdindp1  42418  mapdindp2  42419  mapdindp3  42420  mapdindp4  42421  mapdheq2  42427  mapdheq4lem  42429  mapdheq4  42430  mapdh6lem1N  42431  mapdh6lem2N  42432  mapdh6aN  42433  mapdh6bN  42435  mapdh6cN  42436  mapdh6dN  42437  mapdh6eN  42438  mapdh6fN  42439  mapdh6gN  42440  mapdh6hN  42441  mapdh6iN  42442  mapdh7eN  42446  mapdh7cN  42447  mapdh7dN  42448  mapdh7fN  42449  mapdh75e  42450  mapdh75fN  42453  hvmaplfl  42465  mapdhvmap  42467  mapdh8aa  42474  mapdh8ab  42475  mapdh8ad  42477  mapdh8b  42478  mapdh8c  42479  mapdh8d0N  42480  mapdh8d  42481  mapdh8e  42482  mapdh9a  42487  mapdh9aOLDN  42488  hdmap1val2  42498  hdmap1eq  42499  hdmap1valc  42501  hdmap1eq2  42503  hdmap1eq4N  42504  hdmap1l6lem1  42505  hdmap1l6lem2  42506  hdmap1l6a  42507  hdmap1l6b  42509  hdmap1l6c  42510  hdmap1l6d  42511  hdmap1l6e  42512  hdmap1l6f  42513  hdmap1l6g  42514  hdmap1l6h  42515  hdmap1l6i  42516  hdmap1eulem  42520  hdmap1eulemOLDN  42521  hdmapcl  42528  hdmapval2lem  42529  hdmapval0  42531  hdmapeveclem  42532  hdmapevec  42533  hdmapval3lemN  42535  hdmapval3N  42536  hdmap10lem  42537  hdmap11lem1  42539  hdmap11lem2  42540  hdmapnzcl  42543  hdmaprnlem3N  42548  hdmaprnlem3uN  42549  hdmaprnlem4N  42551  hdmaprnlem7N  42553  hdmaprnlem8N  42554  hdmaprnlem9N  42555  hdmaprnlem3eN  42556  hdmaprnlem16N  42560  hdmap14lem1  42566  hdmap14lem2N  42567  hdmap14lem3  42568  hdmap14lem4a  42569  hdmap14lem6  42571  hdmap14lem8  42573  hdmap14lem9  42574  hdmap14lem10  42575  hdmap14lem11  42576  hdmap14lem12  42577  hgmaprnlem1N  42594  hgmaprnlem2N  42595  hgmaprnlem3N  42596  hgmaprnlem4N  42597  hdmapip1  42614  hdmapinvlem1  42616  hdmapinvlem2  42617  hdmapinvlem3  42618  hdmapinvlem4  42619  hdmapglem5  42620  hgmapvvlem1  42621  hgmapvvlem2  42622  hgmapvvlem3  42623  hdmapglem7a  42625  hdmapglem7b  42626  hdmapglem7  42627  evl1gprodd  42808  nelsubginvcld  43194  nelsubgcld  43195  nelsubgsubcld  43196  domnexpgn0cl  43217  fidomncyc  43229  prjspnfv01  43282  prjspner01  43283  prjspner1  43284  dffltz  43292  qirropth  43561  rmxyneg  43573  rmxm1  43587  rmxluc  43589  rmxdbl  43592  ltrmxnn0  43602  jm2.19lem1  43642  jm2.23  43649  rmxdiophlem  43668  aomclem2  43708  cantnftermord  43973  inaex  44933  bccm1k  44978  dstregt0  45927  fprodexp  46236  fprodabs2  46237  mccllem  46239  fprodcnlem  46241  climrec  46245  climdivf  46254  islpcn  46279  lptre2pt  46280  0ellimcdiv  46289  reclimc  46293  divlimc  46296  cncficcgt0  46528  dvdivf  46562  stoweidlem34  46674  stoweidlem43  46683  etransclem46  46920  etransclem47  46921  etransclem48  46922  hsphoidmvle2  47225  hsphoidmvle  47226  hoidmvlelem3  47237  hoidmvlelem4  47238  hspdifhsp  47256  readdcnnred  47963  resubcnnred  47964  recnmulnred  47965  cndivrenred  47966