Theorem eldifad 3915

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

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

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 3438  df-dif 3906

This theorem is referenced by:  xpdifid  6117  fvdifsupp  8104  unblem1  9181  cantnflem3  9587  cantnflem4  9588  oef1o  9594  infxpenc  9912  acndom2  9948  ackbij1lem18  10130  infpssrlem3  10199  fin23lem26  10219  fin23lem30  10236  pwfseqlem4a  10555  expclz  13991  symgextf  19296  pmtrfinv  19340  symggen  19349  efgsdmi  19611  efgs1b  19615  efgsp1  19616  efgsres  19617  efgredlemf  19620  efgredlemd  19623  efgredlemc  19624  efgredlem  19626  efgrelexlemb  19629  gsum2d2lem  19852  pgpfac1lem2  19956  pgpfac1lem3a  19957  pgpfac1lem3  19958  pgpfac1lem4  19959  zrzeroorngc  20529  zrtermoringc  20560  zrninitoringc  20561  domneq0r  20609  isdrng2  20628  fidomndrnglem  20657  lvecinv  21020  lspsncmp  21023  lspsnne1  21024  lspsnnecom  21026  lspabs2  21027  lspsneu  21030  lspdisjb  21033  lspexch  21036  lspindp1  21040  lvecindp2  21046  lspsolv  21050  lspsnat  21052  lsppratlem1  21054  lsppratlem2  21055  nzerooringczr  21387  frlmssuvc2  21702  evls1fpws  22254  maducoeval2  22525  hauscmplem  23291  1stccnp  23347  imasdsf1olem  24259  rrxmetlem  25305  divcncf  25346  dvrec  25857  dvmptdiv  25876  ftc1lem6  25946  elqaalem1  26225  elqaalem3  26227  ulmdvlem3  26309  abelthlem6  26344  abelthlem7a  26345  abelthlem7  26346  logtayl  26567  dmgmn0  26934  dmgmaddnn0  26935  dmgmdivn0  26936  lgamgulmlem2  26938  lgamgulmlem3  26939  lgamgulmlem5  26941  lgamgulmlem6  26942  lgamgulm2  26944  lgambdd  26945  lgamucov  26946  lgamcvg2  26963  gamcvg  26964  gamcvg2lem  26967  ftalem3  26983  lgsqrlem1  27255  lgsqrlem2  27256  lgsqrlem3  27257  lgsqrlem4  27258  lgseisenlem1  27284  lgseisenlem2  27285  lgseisenlem3  27286  lgseisenlem4  27287  lgseisen  27288  lgsquadlem1  27289  lgsquadlem2  27290  lgsquadlem3  27291  chebbnd1lem1  27378  dchrisum0re  27422  dchrisum0lema  27423  dchrisum0lem1b  27424  dchrisum0lem1  27425  dchrisum0lem2a  27426  dchrisum0lem2  27427  tgisline  28576  elntg  28933  uhgrss  29013  upgrex  29041  edguhgr  29078  1loopgrvd0  29454  disjiunel  32545  suppovss  32631  elfzodif0  32746  nn0difffzod  32758  pfxchn  32960  chnind  32962  chnccats1  32966  gsumfs2d  33017  gsumhashmul  33023  odpmco  33037  pmtrcnel  33040  pmtrcnelor  33042  cycpmco2f1  33075  cycpmco2rn  33076  cycpmco2lem1  33077  cycpmco2lem2  33078  cycpmco2lem3  33079  cycpmco2lem4  33080  cycpmco2lem5  33081  cycpmco2lem6  33082  cycpmco2lem7  33083  cycpmco2  33084  cyc3co2  33091  tocyccntz  33095  cyc3conja  33108  fxpsdrg  33126  elrgspnlem2  33192  elrgspnlem4  33194  elrgspnsubrunlem2  33197  domnprodn0  33224  idomrcanOLD  33230  isdrng4  33243  fracfld  33256  lindssn  33324  lindfpropd  33328  elrspunidl  33374  elrspunsn  33375  drngidl  33379  mxidlmaxv  33414  mxidlirredi  33417  opprqusdrng  33439  qsdrnglem2  33442  rprmcl  33464  rprmirred  33477  pidufd  33489  1arithufdlem3  33492  dfufd2  33496  zringfrac  33500  ply1dg3rt0irred  33527  gsummoncoe1fzo  33539  mplvrpmrhm  33558  lindsunlem  33607  fedgmullem1  33612  fedgmullem2  33613  assafld  33620  fldextrspunlsp  33657  extdgfialglem2  33676  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  35099  iprodgam  35735  poimirlem2  37622  rrndstprj2  37831  lsatelbN  39005  lsatfixedN  39008  lkreqN  39169  lkrlspeqN  39170  dochnel2  41391  dochnel  41392  djhcvat42  41414  dochsnshp  41452  dochexmidat  41458  dochsnkr  41471  dochsnkr2  41472  dochsnkr2cl  41473  dochflcl  41474  dochfl1  41475  dochfln0  41476  lcfl6lem  41497  lcfl7lem  41498  lcfl8b  41503  lclkrlem2a  41506  lclkrlem2b  41507  lclkrlem2c  41508  lclkrlem2d  41509  lclkrlem2e  41510  lclkrlem2f  41511  lcfrlem14  41555  lcfrlem15  41556  lcfrlem16  41557  lcfrlem17  41558  lcfrlem18  41559  lcfrlem19  41560  lcfrlem20  41561  lcfrlem21  41562  lcfrlem23  41564  lcfrlem25  41566  lcfrlem26  41567  lcfrlem35  41576  lcfrlem36  41577  mapdn0  41668  mapdpglem29  41699  mapdpglem24  41703  baerlem3lem1  41706  baerlem5alem1  41707  baerlem5blem1  41708  baerlem3lem2  41709  baerlem5alem2  41710  baerlem5blem2  41711  baerlem5amN  41715  baerlem5bmN  41716  baerlem5abmN  41717  mapdindp0  41718  mapdindp1  41719  mapdindp2  41720  mapdindp3  41721  mapdindp4  41722  mapdheq2  41728  mapdheq4lem  41730  mapdheq4  41731  mapdh6lem1N  41732  mapdh6lem2N  41733  mapdh6aN  41734  mapdh6bN  41736  mapdh6cN  41737  mapdh6dN  41738  mapdh6eN  41739  mapdh6fN  41740  mapdh6gN  41741  mapdh6hN  41742  mapdh6iN  41743  mapdh7eN  41747  mapdh7cN  41748  mapdh7dN  41749  mapdh7fN  41750  mapdh75e  41751  mapdh75fN  41754  hvmaplfl  41766  mapdhvmap  41768  mapdh8aa  41775  mapdh8ab  41776  mapdh8ad  41778  mapdh8b  41779  mapdh8c  41780  mapdh8d0N  41781  mapdh8d  41782  mapdh8e  41783  mapdh9a  41788  mapdh9aOLDN  41789  hdmap1val2  41799  hdmap1eq  41800  hdmap1valc  41802  hdmap1eq2  41804  hdmap1eq4N  41805  hdmap1l6lem1  41806  hdmap1l6lem2  41807  hdmap1l6a  41808  hdmap1l6b  41810  hdmap1l6c  41811  hdmap1l6d  41812  hdmap1l6e  41813  hdmap1l6f  41814  hdmap1l6g  41815  hdmap1l6h  41816  hdmap1l6i  41817  hdmap1eulem  41821  hdmap1eulemOLDN  41822  hdmapcl  41829  hdmapval2lem  41830  hdmapval0  41832  hdmapeveclem  41833  hdmapevec  41834  hdmapval3lemN  41836  hdmapval3N  41837  hdmap10lem  41838  hdmap11lem1  41840  hdmap11lem2  41841  hdmapnzcl  41844  hdmaprnlem3N  41849  hdmaprnlem3uN  41850  hdmaprnlem4N  41852  hdmaprnlem7N  41854  hdmaprnlem8N  41855  hdmaprnlem9N  41856  hdmaprnlem3eN  41857  hdmaprnlem16N  41861  hdmap14lem1  41867  hdmap14lem2N  41868  hdmap14lem3  41869  hdmap14lem4a  41870  hdmap14lem6  41872  hdmap14lem8  41874  hdmap14lem9  41875  hdmap14lem10  41876  hdmap14lem11  41877  hdmap14lem12  41878  hgmaprnlem1N  41895  hgmaprnlem2N  41896  hgmaprnlem3N  41897  hgmaprnlem4N  41898  hdmapip1  41915  hdmapinvlem1  41917  hdmapinvlem2  41918  hdmapinvlem3  41919  hdmapinvlem4  41920  hdmapglem5  41921  hgmapvvlem1  41922  hgmapvvlem2  41923  hgmapvvlem3  41924  hdmapglem7a  41926  hdmapglem7b  41927  hdmapglem7  41928  evl1gprodd  42110  nelsubginvcld  42489  nelsubgcld  42490  nelsubgsubcld  42491  domnexpgn0cl  42516  fidomncyc  42528  prjspnfv01  42617  prjspner01  42618  prjspner1  42619  dffltz  42627  qirropth  42901  rmxyneg  42913  rmxm1  42927  rmxluc  42929  rmxdbl  42932  ltrmxnn0  42942  jm2.19lem1  42982  jm2.23  42989  rmxdiophlem  43008  aomclem2  43048  cantnftermord  43313  inaex  44290  bccm1k  44335  dstregt0  45284  fprodexp  45595  fprodabs2  45596  mccllem  45598  fprodcnlem  45600  climrec  45604  climdivf  45613  islpcn  45640  lptre2pt  45641  0ellimcdiv  45650  reclimc  45654  divlimc  45657  cncficcgt0  45889  dvdivf  45923  stoweidlem34  46035  stoweidlem43  46044  etransclem46  46281  etransclem47  46282  etransclem48  46283  hsphoidmvle2  46586  hsphoidmvle  46587  hoidmvlelem3  46598  hoidmvlelem4  46599  hspdifhsp  46617  readdcnnred  47307  resubcnnred  47308  recnmulnred  47309  cndivrenred  47310