Theorem eldifad 3923

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-dif 3914

This theorem is referenced by:  xpdifid  6129  fvdifsupp  8127  unblem1  9215  cantnflem3  9620  cantnflem4  9621  oef1o  9627  infxpenc  9947  acndom2  9983  ackbij1lem18  10165  infpssrlem3  10234  fin23lem26  10254  fin23lem30  10271  pwfseqlem4a  10590  expclz  14025  symgextf  19331  pmtrfinv  19375  symggen  19384  efgsdmi  19646  efgs1b  19650  efgsp1  19651  efgsres  19652  efgredlemf  19655  efgredlemd  19658  efgredlemc  19659  efgredlem  19661  efgrelexlemb  19664  gsum2d2lem  19887  pgpfac1lem2  19991  pgpfac1lem3a  19992  pgpfac1lem3  19993  pgpfac1lem4  19994  zrzeroorngc  20564  zrtermoringc  20595  zrninitoringc  20596  domneq0r  20644  isdrng2  20663  fidomndrnglem  20692  lvecinv  21055  lspsncmp  21058  lspsnne1  21059  lspsnnecom  21061  lspabs2  21062  lspsneu  21065  lspdisjb  21068  lspexch  21071  lspindp1  21075  lvecindp2  21081  lspsolv  21085  lspsnat  21087  lsppratlem1  21089  lsppratlem2  21090  nzerooringczr  21422  frlmssuvc2  21737  evls1fpws  22289  maducoeval2  22560  hauscmplem  23326  1stccnp  23382  imasdsf1olem  24294  rrxmetlem  25340  divcncf  25381  dvrec  25892  dvmptdiv  25911  ftc1lem6  25981  elqaalem1  26260  elqaalem3  26262  ulmdvlem3  26344  abelthlem6  26379  abelthlem7a  26380  abelthlem7  26381  logtayl  26602  dmgmn0  26969  dmgmaddnn0  26970  dmgmdivn0  26971  lgamgulmlem2  26973  lgamgulmlem3  26974  lgamgulmlem5  26976  lgamgulmlem6  26977  lgamgulm2  26979  lgambdd  26980  lgamucov  26981  lgamcvg2  26998  gamcvg  26999  gamcvg2lem  27002  ftalem3  27018  lgsqrlem1  27290  lgsqrlem2  27291  lgsqrlem3  27292  lgsqrlem4  27293  lgseisenlem1  27319  lgseisenlem2  27320  lgseisenlem3  27321  lgseisenlem4  27322  lgseisen  27323  lgsquadlem1  27324  lgsquadlem2  27325  lgsquadlem3  27326  chebbnd1lem1  27413  dchrisum0re  27457  dchrisum0lema  27458  dchrisum0lem1b  27459  dchrisum0lem1  27460  dchrisum0lem2a  27461  dchrisum0lem2  27462  tgisline  28607  elntg  28964  uhgrss  29044  upgrex  29072  edguhgr  29109  1loopgrvd0  29485  disjiunel  32575  suppovss  32654  elfzodif0  32767  nn0difffzod  32779  pfxchn  32981  chnind  32983  chnccats1  32987  gsumfs2d  33038  gsumhashmul  33044  odpmco  33058  pmtrcnel  33061  pmtrcnelor  33063  cycpmco2f1  33096  cycpmco2rn  33097  cycpmco2lem1  33098  cycpmco2lem2  33099  cycpmco2lem3  33100  cycpmco2lem4  33101  cycpmco2lem5  33102  cycpmco2lem6  33103  cycpmco2lem7  33104  cycpmco2  33105  cyc3co2  33112  tocyccntz  33116  cyc3conja  33129  elrgspnlem2  33210  elrgspnlem4  33212  elrgspnsubrunlem2  33215  domnprodn0  33242  idomrcanOLD  33248  isdrng4  33261  fracfld  33274  lindssn  33342  lindfpropd  33346  elrspunidl  33392  elrspunsn  33393  drngidl  33397  mxidlmaxv  33432  mxidlirredi  33435  opprqusdrng  33457  qsdrnglem2  33460  rprmcl  33482  rprmirred  33495  pidufd  33507  1arithufdlem3  33510  dfufd2  33514  zringfrac  33518  ply1dg3rt0irred  33544  gsummoncoe1fzo  33556  lindsunlem  33613  fedgmullem1  33618  fedgmullem2  33619  assafld  33626  fldextrspunlsp  33662  irngnminplynz  33695  constrextdg2lem  33731  constrfiss  33734  constrsdrg  33758  submatminr1  33793  qtophaus  33819  qqhval2  33965  esummono  34037  gsumesum  34042  esum2dlem  34075  measvuni  34197  fiunelcarsg  34300  sitgclg  34326  sitgaddlemb  34332  eulerpartlemsv2  34342  eulerpartlemsv3  34345  eulerpartlemgc  34346  eulerpartlemv  34348  signstfvneq0  34556  signstfvcl  34557  signstfveq0a  34560  signstfveq0  34561  signsvfn  34566  signsvtp  34567  signsvtn  34568  signsvfpn  34569  signsvfnn  34570  signlem0  34571  hgt750leme  34642  onvf1odlem4  35086  iprodgam  35722  poimirlem2  37609  rrndstprj2  37818  lsatelbN  38992  lsatfixedN  38995  lkreqN  39156  lkrlspeqN  39157  dochnel2  41379  dochnel  41380  djhcvat42  41402  dochsnshp  41440  dochexmidat  41446  dochsnkr  41459  dochsnkr2  41460  dochsnkr2cl  41461  dochflcl  41462  dochfl1  41463  dochfln0  41464  lcfl6lem  41485  lcfl7lem  41486  lcfl8b  41491  lclkrlem2a  41494  lclkrlem2b  41495  lclkrlem2c  41496  lclkrlem2d  41497  lclkrlem2e  41498  lclkrlem2f  41499  lcfrlem14  41543  lcfrlem15  41544  lcfrlem16  41545  lcfrlem17  41546  lcfrlem18  41547  lcfrlem19  41548  lcfrlem20  41549  lcfrlem21  41550  lcfrlem23  41552  lcfrlem25  41554  lcfrlem26  41555  lcfrlem35  41564  lcfrlem36  41565  mapdn0  41656  mapdpglem29  41687  mapdpglem24  41691  baerlem3lem1  41694  baerlem5alem1  41695  baerlem5blem1  41696  baerlem3lem2  41697  baerlem5alem2  41698  baerlem5blem2  41699  baerlem5amN  41703  baerlem5bmN  41704  baerlem5abmN  41705  mapdindp0  41706  mapdindp1  41707  mapdindp2  41708  mapdindp3  41709  mapdindp4  41710  mapdheq2  41716  mapdheq4lem  41718  mapdheq4  41719  mapdh6lem1N  41720  mapdh6lem2N  41721  mapdh6aN  41722  mapdh6bN  41724  mapdh6cN  41725  mapdh6dN  41726  mapdh6eN  41727  mapdh6fN  41728  mapdh6gN  41729  mapdh6hN  41730  mapdh6iN  41731  mapdh7eN  41735  mapdh7cN  41736  mapdh7dN  41737  mapdh7fN  41738  mapdh75e  41739  mapdh75fN  41742  hvmaplfl  41754  mapdhvmap  41756  mapdh8aa  41763  mapdh8ab  41764  mapdh8ad  41766  mapdh8b  41767  mapdh8c  41768  mapdh8d0N  41769  mapdh8d  41770  mapdh8e  41771  mapdh9a  41776  mapdh9aOLDN  41777  hdmap1val2  41787  hdmap1eq  41788  hdmap1valc  41790  hdmap1eq2  41792  hdmap1eq4N  41793  hdmap1l6lem1  41794  hdmap1l6lem2  41795  hdmap1l6a  41796  hdmap1l6b  41798  hdmap1l6c  41799  hdmap1l6d  41800  hdmap1l6e  41801  hdmap1l6f  41802  hdmap1l6g  41803  hdmap1l6h  41804  hdmap1l6i  41805  hdmap1eulem  41809  hdmap1eulemOLDN  41810  hdmapcl  41817  hdmapval2lem  41818  hdmapval0  41820  hdmapeveclem  41821  hdmapevec  41822  hdmapval3lemN  41824  hdmapval3N  41825  hdmap10lem  41826  hdmap11lem1  41828  hdmap11lem2  41829  hdmapnzcl  41832  hdmaprnlem3N  41837  hdmaprnlem3uN  41838  hdmaprnlem4N  41840  hdmaprnlem7N  41842  hdmaprnlem8N  41843  hdmaprnlem9N  41844  hdmaprnlem3eN  41845  hdmaprnlem16N  41849  hdmap14lem1  41855  hdmap14lem2N  41856  hdmap14lem3  41857  hdmap14lem4a  41858  hdmap14lem6  41860  hdmap14lem8  41862  hdmap14lem9  41863  hdmap14lem10  41864  hdmap14lem11  41865  hdmap14lem12  41866  hgmaprnlem1N  41883  hgmaprnlem2N  41884  hgmaprnlem3N  41885  hgmaprnlem4N  41886  hdmapip1  41903  hdmapinvlem1  41905  hdmapinvlem2  41906  hdmapinvlem3  41907  hdmapinvlem4  41908  hdmapglem5  41909  hgmapvvlem1  41910  hgmapvvlem2  41911  hgmapvvlem3  41912  hdmapglem7a  41914  hdmapglem7b  41915  hdmapglem7  41916  evl1gprodd  42098  nelsubginvcld  42477  nelsubgcld  42478  nelsubgsubcld  42479  domnexpgn0cl  42504  fidomncyc  42516  prjspnfv01  42605  prjspner01  42606  prjspner1  42607  dffltz  42615  qirropth  42889  rmxyneg  42902  rmxm1  42916  rmxluc  42918  rmxdbl  42921  ltrmxnn0  42931  jm2.19lem1  42971  jm2.23  42978  rmxdiophlem  42997  aomclem2  43037  cantnftermord  43302  inaex  44279  bccm1k  44324  dstregt0  45273  fprodexp  45585  fprodabs2  45586  mccllem  45588  fprodcnlem  45590  climrec  45594  climdivf  45603  islpcn  45630  lptre2pt  45631  0ellimcdiv  45640  reclimc  45644  divlimc  45647  cncficcgt0  45879  dvdivf  45913  stoweidlem34  46025  stoweidlem43  46034  etransclem46  46271  etransclem47  46272  etransclem48  46273  hsphoidmvle2  46576  hsphoidmvle  46577  hoidmvlelem3  46588  hoidmvlelem4  46589  hspdifhsp  46607  readdcnnred  47297  resubcnnred  47298  recnmulnred  47299  cndivrenred  47300