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 218	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))
4	3	simpld 494	1 ⊢ (𝜑 → 𝐴 ∈ 𝐵)

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

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 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-dif 3902

This theorem is referenced by:  xpdifid  6124  fvdifsupp  8111  unblem1  9190  cantnflem3  9598  cantnflem4  9599  oef1o  9605  infxpenc  9926  acndom2  9962  ackbij1lem18  10144  infpssrlem3  10213  fin23lem26  10233  fin23lem30  10250  pwfseqlem4a  10570  elfzodif0  13684  expclz  14005  pfxchn  18531  chnind  18542  chnccats1  18546  chnccat  18547  symgextf  19344  pmtrfinv  19388  symggen  19397  efgsdmi  19659  efgs1b  19663  efgsp1  19664  efgsres  19665  efgredlemf  19668  efgredlemd  19671  efgredlemc  19672  efgredlem  19674  efgrelexlemb  19677  gsum2d2lem  19900  pgpfac1lem2  20004  pgpfac1lem3a  20005  pgpfac1lem3  20006  pgpfac1lem4  20007  zrzeroorngc  20575  zrtermoringc  20606  zrninitoringc  20607  domneq0r  20655  isdrng2  20674  fidomndrnglem  20703  lvecinv  21066  lspsncmp  21069  lspsnne1  21070  lspsnnecom  21072  lspabs2  21073  lspsneu  21076  lspdisjb  21079  lspexch  21082  lspindp1  21086  lvecindp2  21092  lspsolv  21096  lspsnat  21098  lsppratlem1  21100  lsppratlem2  21101  nzerooringczr  21433  frlmssuvc2  21748  evls1fpws  22311  maducoeval2  22582  hauscmplem  23348  1stccnp  23404  imasdsf1olem  24315  rrxmetlem  25361  divcncf  25402  dvrec  25913  dvmptdiv  25932  ftc1lem6  26002  elqaalem1  26281  elqaalem3  26283  ulmdvlem3  26365  abelthlem6  26400  abelthlem7a  26401  abelthlem7  26402  logtayl  26623  dmgmn0  26990  dmgmaddnn0  26991  dmgmdivn0  26992  lgamgulmlem2  26994  lgamgulmlem3  26995  lgamgulmlem5  26997  lgamgulmlem6  26998  lgamgulm2  27000  lgambdd  27001  lgamucov  27002  lgamcvg2  27019  gamcvg  27020  gamcvg2lem  27023  ftalem3  27039  lgsqrlem1  27311  lgsqrlem2  27312  lgsqrlem3  27313  lgsqrlem4  27314  lgseisenlem1  27340  lgseisenlem2  27341  lgseisenlem3  27342  lgseisenlem4  27343  lgseisen  27344  lgsquadlem1  27345  lgsquadlem2  27346  lgsquadlem3  27347  chebbnd1lem1  27434  dchrisum0re  27478  dchrisum0lema  27479  dchrisum0lem1b  27480  dchrisum0lem1  27481  dchrisum0lem2a  27482  dchrisum0lem2  27483  tgisline  28648  elntg  29006  uhgrss  29086  upgrex  29114  edguhgr  29151  1loopgrvd0  29527  disjiunel  32620  suppovss  32709  nn0difffzod  32833  gsumfs2d  33093  gsumhashmul  33099  odpmco  33117  pmtrcnel  33120  pmtrcnelor  33122  cycpmco2f1  33155  cycpmco2rn  33156  cycpmco2lem1  33157  cycpmco2lem2  33158  cycpmco2lem3  33159  cycpmco2lem4  33160  cycpmco2lem5  33161  cycpmco2lem6  33162  cycpmco2lem7  33163  cycpmco2  33164  cyc3co2  33171  tocyccntz  33175  cyc3conja  33188  fxpsdrg  33206  elrgspnlem2  33274  elrgspnlem4  33276  elrgspnsubrunlem2  33279  domnprodn0  33306  domnprodeq0  33307  idomrcanOLD  33313  isdrng4  33326  fracfld  33339  lindssn  33408  lindfpropd  33412  elrspunidl  33458  elrspunsn  33459  drngidl  33463  mxidlmaxv  33498  mxidlirredi  33501  opprqusdrng  33523  qsdrnglem2  33526  rprmcl  33548  rprmirred  33561  pidufd  33573  1arithufdlem3  33576  dfufd2  33580  zringfrac  33584  deg1prod  33613  ply1dg3rt0irred  33614  gsummoncoe1fzo  33627  mplvrpmrhm  33661  esplyfval2  33672  lindsunlem  33730  fedgmullem1  33735  fedgmullem2  33736  assafld  33743  fldextrspunlsp  33780  extdgfialglem2  33799  irngnminplynz  33818  constrextdg2lem  33854  constrfiss  33857  constrsdrg  33881  submatminr1  33916  qtophaus  33942  qqhval2  34088  esummono  34160  gsumesum  34165  esum2dlem  34198  measvuni  34320  fiunelcarsg  34422  sitgclg  34448  sitgaddlemb  34454  eulerpartlemsv2  34464  eulerpartlemsv3  34467  eulerpartlemgc  34468  eulerpartlemv  34470  signstfvneq0  34678  signstfvcl  34679  signstfveq0a  34682  signstfveq0  34683  signsvfn  34688  signsvtp  34689  signsvtn  34690  signsvfpn  34691  signsvfnn  34692  signlem0  34693  hgt750leme  34764  onvf1odlem4  35249  iprodgam  35885  poimirlem2  37762  rrndstprj2  37971  lsatelbN  39205  lsatfixedN  39208  lkreqN  39369  lkrlspeqN  39370  dochnel2  41591  dochnel  41592  djhcvat42  41614  dochsnshp  41652  dochexmidat  41658  dochsnkr  41671  dochsnkr2  41672  dochsnkr2cl  41673  dochflcl  41674  dochfl1  41675  dochfln0  41676  lcfl6lem  41697  lcfl7lem  41698  lcfl8b  41703  lclkrlem2a  41706  lclkrlem2b  41707  lclkrlem2c  41708  lclkrlem2d  41709  lclkrlem2e  41710  lclkrlem2f  41711  lcfrlem14  41755  lcfrlem15  41756  lcfrlem16  41757  lcfrlem17  41758  lcfrlem18  41759  lcfrlem19  41760  lcfrlem20  41761  lcfrlem21  41762  lcfrlem23  41764  lcfrlem25  41766  lcfrlem26  41767  lcfrlem35  41776  lcfrlem36  41777  mapdn0  41868  mapdpglem29  41899  mapdpglem24  41903  baerlem3lem1  41906  baerlem5alem1  41907  baerlem5blem1  41908  baerlem3lem2  41909  baerlem5alem2  41910  baerlem5blem2  41911  baerlem5amN  41915  baerlem5bmN  41916  baerlem5abmN  41917  mapdindp0  41918  mapdindp1  41919  mapdindp2  41920  mapdindp3  41921  mapdindp4  41922  mapdheq2  41928  mapdheq4lem  41930  mapdheq4  41931  mapdh6lem1N  41932  mapdh6lem2N  41933  mapdh6aN  41934  mapdh6bN  41936  mapdh6cN  41937  mapdh6dN  41938  mapdh6eN  41939  mapdh6fN  41940  mapdh6gN  41941  mapdh6hN  41942  mapdh6iN  41943  mapdh7eN  41947  mapdh7cN  41948  mapdh7dN  41949  mapdh7fN  41950  mapdh75e  41951  mapdh75fN  41954  hvmaplfl  41966  mapdhvmap  41968  mapdh8aa  41975  mapdh8ab  41976  mapdh8ad  41978  mapdh8b  41979  mapdh8c  41980  mapdh8d0N  41981  mapdh8d  41982  mapdh8e  41983  mapdh9a  41988  mapdh9aOLDN  41989  hdmap1val2  41999  hdmap1eq  42000  hdmap1valc  42002  hdmap1eq2  42004  hdmap1eq4N  42005  hdmap1l6lem1  42006  hdmap1l6lem2  42007  hdmap1l6a  42008  hdmap1l6b  42010  hdmap1l6c  42011  hdmap1l6d  42012  hdmap1l6e  42013  hdmap1l6f  42014  hdmap1l6g  42015  hdmap1l6h  42016  hdmap1l6i  42017  hdmap1eulem  42021  hdmap1eulemOLDN  42022  hdmapcl  42029  hdmapval2lem  42030  hdmapval0  42032  hdmapeveclem  42033  hdmapevec  42034  hdmapval3lemN  42036  hdmapval3N  42037  hdmap10lem  42038  hdmap11lem1  42040  hdmap11lem2  42041  hdmapnzcl  42044  hdmaprnlem3N  42049  hdmaprnlem3uN  42050  hdmaprnlem4N  42052  hdmaprnlem7N  42054  hdmaprnlem8N  42055  hdmaprnlem9N  42056  hdmaprnlem3eN  42057  hdmaprnlem16N  42061  hdmap14lem1  42067  hdmap14lem2N  42068  hdmap14lem3  42069  hdmap14lem4a  42070  hdmap14lem6  42072  hdmap14lem8  42074  hdmap14lem9  42075  hdmap14lem10  42076  hdmap14lem11  42077  hdmap14lem12  42078  hgmaprnlem1N  42095  hgmaprnlem2N  42096  hgmaprnlem3N  42097  hgmaprnlem4N  42098  hdmapip1  42115  hdmapinvlem1  42117  hdmapinvlem2  42118  hdmapinvlem3  42119  hdmapinvlem4  42120  hdmapglem5  42121  hgmapvvlem1  42122  hgmapvvlem2  42123  hgmapvvlem3  42124  hdmapglem7a  42126  hdmapglem7b  42127  hdmapglem7  42128  evl1gprodd  42310  nelsubginvcld  42693  nelsubgcld  42694  nelsubgsubcld  42695  domnexpgn0cl  42720  fidomncyc  42732  prjspnfv01  42809  prjspner01  42810  prjspner1  42811  dffltz  42819  qirropth  43092  rmxyneg  43104  rmxm1  43118  rmxluc  43120  rmxdbl  43123  ltrmxnn0  43133  jm2.19lem1  43173  jm2.23  43180  rmxdiophlem  43199  aomclem2  43239  cantnftermord  43504  inaex  44480  bccm1k  44525  dstregt0  45472  fprodexp  45782  fprodabs2  45783  mccllem  45785  fprodcnlem  45787  climrec  45791  climdivf  45800  islpcn  45825  lptre2pt  45826  0ellimcdiv  45835  reclimc  45839  divlimc  45842  cncficcgt0  46074  dvdivf  46108  stoweidlem34  46220  stoweidlem43  46229  etransclem46  46466  etransclem47  46467  etransclem48  46468  hsphoidmvle2  46771  hsphoidmvle  46772  hoidmvlelem3  46783  hoidmvlelem4  46784  hspdifhsp  46802  readdcnnred  47491  resubcnnred  47492  recnmulnred  47493  cndivrenred  47494