Theorem eldifad 3963

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954

This theorem is referenced by:  xpdifid  6188  fvdifsupp  8196  unblem1  9328  cantnflem3  9731  cantnflem4  9732  oef1o  9738  infxpenc  10058  acndom2  10094  ackbij1lem18  10276  infpssrlem3  10345  fin23lem26  10365  fin23lem30  10382  pwfseqlem4a  10701  expclz  14125  symgextf  19435  pmtrfinv  19479  symggen  19488  efgsdmi  19750  efgs1b  19754  efgsp1  19755  efgsres  19756  efgredlemf  19759  efgredlemd  19762  efgredlemc  19763  efgredlem  19765  efgrelexlemb  19768  gsum2d2lem  19991  pgpfac1lem2  20095  pgpfac1lem3a  20096  pgpfac1lem3  20097  pgpfac1lem4  20098  zrzeroorngc  20644  zrtermoringc  20675  zrninitoringc  20676  domneq0r  20724  isdrng2  20743  fidomndrnglem  20773  lvecinv  21115  lspsncmp  21118  lspsnne1  21119  lspsnnecom  21121  lspabs2  21122  lspsneu  21125  lspdisjb  21128  lspexch  21131  lspindp1  21135  lvecindp2  21141  lspsolv  21145  lspsnat  21147  lsppratlem1  21149  lsppratlem2  21150  nzerooringczr  21491  frlmssuvc2  21815  evls1fpws  22373  maducoeval2  22646  hauscmplem  23414  1stccnp  23470  imasdsf1olem  24383  rrxmetlem  25441  divcncf  25482  dvrec  25993  dvmptdiv  26012  ftc1lem6  26082  elqaalem1  26361  elqaalem3  26363  ulmdvlem3  26445  abelthlem6  26480  abelthlem7a  26481  abelthlem7  26482  logtayl  26702  dmgmn0  27069  dmgmaddnn0  27070  dmgmdivn0  27071  lgamgulmlem2  27073  lgamgulmlem3  27074  lgamgulmlem5  27076  lgamgulmlem6  27077  lgamgulm2  27079  lgambdd  27080  lgamucov  27081  lgamcvg2  27098  gamcvg  27099  gamcvg2lem  27102  ftalem3  27118  lgsqrlem1  27390  lgsqrlem2  27391  lgsqrlem3  27392  lgsqrlem4  27393  lgseisenlem1  27419  lgseisenlem2  27420  lgseisenlem3  27421  lgseisenlem4  27422  lgseisen  27423  lgsquadlem1  27424  lgsquadlem2  27425  lgsquadlem3  27426  chebbnd1lem1  27513  dchrisum0re  27557  dchrisum0lema  27558  dchrisum0lem1b  27559  dchrisum0lem1  27560  dchrisum0lem2a  27561  dchrisum0lem2  27562  tgisline  28635  elntg  28999  uhgrss  29081  upgrex  29109  edguhgr  29146  1loopgrvd0  29522  disjiunel  32609  suppovss  32690  elfzodif0  32796  nn0difffzod  32808  pfxchn  32999  chnind  33001  chnccats1  33005  gsumfs2d  33058  gsumhashmul  33064  odpmco  33106  pmtrcnel  33109  pmtrcnelor  33111  cycpmco2f1  33144  cycpmco2rn  33145  cycpmco2lem1  33146  cycpmco2lem2  33147  cycpmco2lem3  33148  cycpmco2lem4  33149  cycpmco2lem5  33150  cycpmco2lem6  33151  cycpmco2lem7  33152  cycpmco2  33153  cyc3co2  33160  tocyccntz  33164  cyc3conja  33177  elrgspnlem2  33247  elrgspnlem4  33249  elrgspnsubrunlem2  33252  domnprodn0  33279  idomrcanOLD  33285  isdrng4  33298  fracfld  33310  lindssn  33406  lindfpropd  33410  elrspunidl  33456  elrspunsn  33457  drngidl  33461  mxidlmaxv  33496  mxidlirredi  33499  opprqusdrng  33521  qsdrnglem2  33524  rprmcl  33546  rprmirred  33559  pidufd  33571  1arithufdlem3  33574  dfufd2  33578  zringfrac  33582  ply1dg3rt0irred  33607  gsummoncoe1fzo  33618  lindsunlem  33675  fedgmullem1  33680  fedgmullem2  33681  assafld  33688  fldextrspunlsp  33724  irngnminplynz  33755  constrextdg2lem  33789  submatminr1  33809  qtophaus  33835  qqhval2  33983  esummono  34055  gsumesum  34060  esum2dlem  34093  measvuni  34215  fiunelcarsg  34318  sitgclg  34344  sitgaddlemb  34350  eulerpartlemsv2  34360  eulerpartlemsv3  34363  eulerpartlemgc  34364  eulerpartlemv  34366  signstfvneq0  34587  signstfvcl  34588  signstfveq0a  34591  signstfveq0  34592  signsvfn  34597  signsvtp  34598  signsvtn  34599  signsvfpn  34600  signsvfnn  34601  signlem0  34602  hgt750leme  34673  iprodgam  35742  poimirlem2  37629  rrndstprj2  37838  lsatelbN  39007  lsatfixedN  39010  lkreqN  39171  lkrlspeqN  39172  dochnel2  41394  dochnel  41395  djhcvat42  41417  dochsnshp  41455  dochexmidat  41461  dochsnkr  41474  dochsnkr2  41475  dochsnkr2cl  41476  dochflcl  41477  dochfl1  41478  dochfln0  41479  lcfl6lem  41500  lcfl7lem  41501  lcfl8b  41506  lclkrlem2a  41509  lclkrlem2b  41510  lclkrlem2c  41511  lclkrlem2d  41512  lclkrlem2e  41513  lclkrlem2f  41514  lcfrlem14  41558  lcfrlem15  41559  lcfrlem16  41560  lcfrlem17  41561  lcfrlem18  41562  lcfrlem19  41563  lcfrlem20  41564  lcfrlem21  41565  lcfrlem23  41567  lcfrlem25  41569  lcfrlem26  41570  lcfrlem35  41579  lcfrlem36  41580  mapdn0  41671  mapdpglem29  41702  mapdpglem24  41706  baerlem3lem1  41709  baerlem5alem1  41710  baerlem5blem1  41711  baerlem3lem2  41712  baerlem5alem2  41713  baerlem5blem2  41714  baerlem5amN  41718  baerlem5bmN  41719  baerlem5abmN  41720  mapdindp0  41721  mapdindp1  41722  mapdindp2  41723  mapdindp3  41724  mapdindp4  41725  mapdheq2  41731  mapdheq4lem  41733  mapdheq4  41734  mapdh6lem1N  41735  mapdh6lem2N  41736  mapdh6aN  41737  mapdh6bN  41739  mapdh6cN  41740  mapdh6dN  41741  mapdh6eN  41742  mapdh6fN  41743  mapdh6gN  41744  mapdh6hN  41745  mapdh6iN  41746  mapdh7eN  41750  mapdh7cN  41751  mapdh7dN  41752  mapdh7fN  41753  mapdh75e  41754  mapdh75fN  41757  hvmaplfl  41769  mapdhvmap  41771  mapdh8aa  41778  mapdh8ab  41779  mapdh8ad  41781  mapdh8b  41782  mapdh8c  41783  mapdh8d0N  41784  mapdh8d  41785  mapdh8e  41786  mapdh9a  41791  mapdh9aOLDN  41792  hdmap1val2  41802  hdmap1eq  41803  hdmap1valc  41805  hdmap1eq2  41807  hdmap1eq4N  41808  hdmap1l6lem1  41809  hdmap1l6lem2  41810  hdmap1l6a  41811  hdmap1l6b  41813  hdmap1l6c  41814  hdmap1l6d  41815  hdmap1l6e  41816  hdmap1l6f  41817  hdmap1l6g  41818  hdmap1l6h  41819  hdmap1l6i  41820  hdmap1eulem  41824  hdmap1eulemOLDN  41825  hdmapcl  41832  hdmapval2lem  41833  hdmapval0  41835  hdmapeveclem  41836  hdmapevec  41837  hdmapval3lemN  41839  hdmapval3N  41840  hdmap10lem  41841  hdmap11lem1  41843  hdmap11lem2  41844  hdmapnzcl  41847  hdmaprnlem3N  41852  hdmaprnlem3uN  41853  hdmaprnlem4N  41855  hdmaprnlem7N  41857  hdmaprnlem8N  41858  hdmaprnlem9N  41859  hdmaprnlem3eN  41860  hdmaprnlem16N  41864  hdmap14lem1  41870  hdmap14lem2N  41871  hdmap14lem3  41872  hdmap14lem4a  41873  hdmap14lem6  41875  hdmap14lem8  41877  hdmap14lem9  41878  hdmap14lem10  41879  hdmap14lem11  41880  hdmap14lem12  41881  hgmaprnlem1N  41898  hgmaprnlem2N  41899  hgmaprnlem3N  41900  hgmaprnlem4N  41901  hdmapip1  41918  hdmapinvlem1  41920  hdmapinvlem2  41921  hdmapinvlem3  41922  hdmapinvlem4  41923  hdmapglem5  41924  hgmapvvlem1  41925  hgmapvvlem2  41926  hgmapvvlem3  41927  hdmapglem7a  41929  hdmapglem7b  41930  hdmapglem7  41931  evl1gprodd  42118  nelsubginvcld  42506  nelsubgcld  42507  nelsubgsubcld  42508  domnexpgn0cl  42533  fidomncyc  42545  prjspnfv01  42634  prjspner01  42635  prjspner1  42636  dffltz  42644  qirropth  42919  rmxyneg  42932  rmxm1  42946  rmxluc  42948  rmxdbl  42951  ltrmxnn0  42961  jm2.19lem1  43001  jm2.23  43008  rmxdiophlem  43027  aomclem2  43067  cantnftermord  43333  inaex  44316  bccm1k  44361  dstregt0  45293  fprodexp  45609  fprodabs2  45610  mccllem  45612  fprodcnlem  45614  climrec  45618  climdivf  45627  islpcn  45654  lptre2pt  45655  0ellimcdiv  45664  reclimc  45668  divlimc  45671  cncficcgt0  45903  dvdivf  45937  stoweidlem34  46049  stoweidlem43  46058  etransclem46  46295  etransclem47  46296  etransclem48  46297  hsphoidmvle2  46600  hsphoidmvle  46601  hoidmvlelem3  46612  hoidmvlelem4  46613  hspdifhsp  46631  readdcnnred  47315  resubcnnred  47316  recnmulnred  47317  cndivrenred  47318