Theorem eldifad 3988

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979

This theorem is referenced by:  xpdifid  6199  fvdifsupp  8212  unblem1  9356  cantnflem3  9760  cantnflem4  9761  oef1o  9767  infxpenc  10087  acndom2  10123  ackbij1lem18  10305  infpssrlem3  10374  fin23lem26  10394  fin23lem30  10411  pwfseqlem4a  10730  expclz  14135  symgextf  19459  pmtrfinv  19503  symggen  19512  efgsdmi  19774  efgs1b  19778  efgsp1  19779  efgsres  19780  efgredlemf  19783  efgredlemd  19786  efgredlemc  19787  efgredlem  19789  efgrelexlemb  19792  gsum2d2lem  20015  pgpfac1lem2  20119  pgpfac1lem3a  20120  pgpfac1lem3  20121  pgpfac1lem4  20122  zrzeroorngc  20666  zrtermoringc  20697  zrninitoringc  20698  domneq0r  20746  isdrng2  20765  fidomndrnglem  20795  lvecinv  21138  lspsncmp  21141  lspsnne1  21142  lspsnnecom  21144  lspabs2  21145  lspsneu  21148  lspdisjb  21151  lspexch  21154  lspindp1  21158  lvecindp2  21164  lspsolv  21168  lspsnat  21170  lsppratlem1  21172  lsppratlem2  21173  nzerooringczr  21514  frlmssuvc2  21838  evls1fpws  22394  maducoeval2  22667  hauscmplem  23435  1stccnp  23491  imasdsf1olem  24404  rrxmetlem  25460  divcncf  25501  dvrec  26013  dvmptdiv  26032  ftc1lem6  26102  elqaalem1  26379  elqaalem3  26381  ulmdvlem3  26463  abelthlem6  26498  abelthlem7a  26499  abelthlem7  26500  logtayl  26720  dmgmn0  27087  dmgmaddnn0  27088  dmgmdivn0  27089  lgamgulmlem2  27091  lgamgulmlem3  27092  lgamgulmlem5  27094  lgamgulmlem6  27095  lgamgulm2  27097  lgambdd  27098  lgamucov  27099  lgamcvg2  27116  gamcvg  27117  gamcvg2lem  27120  ftalem3  27136  lgsqrlem1  27408  lgsqrlem2  27409  lgsqrlem3  27410  lgsqrlem4  27411  lgseisenlem1  27437  lgseisenlem2  27438  lgseisenlem3  27439  lgseisenlem4  27440  lgseisen  27441  lgsquadlem1  27442  lgsquadlem2  27443  lgsquadlem3  27444  chebbnd1lem1  27531  dchrisum0re  27575  dchrisum0lema  27576  dchrisum0lem1b  27577  dchrisum0lem1  27578  dchrisum0lem2a  27579  dchrisum0lem2  27580  tgisline  28653  elntg  29017  uhgrss  29099  upgrex  29127  edguhgr  29164  1loopgrvd0  29540  disjiunel  32618  suppovss  32697  nn0difffzod  32811  pfxchn  32982  chnind  32983  gsumhashmul  33040  odpmco  33079  pmtrcnel  33082  pmtrcnelor  33084  cycpmco2f1  33117  cycpmco2rn  33118  cycpmco2lem1  33119  cycpmco2lem2  33120  cycpmco2lem3  33121  cycpmco2lem4  33122  cycpmco2lem5  33123  cycpmco2lem6  33124  cycpmco2lem7  33125  cycpmco2  33126  cyc3co2  33133  tocyccntz  33137  cyc3conja  33150  domnprodn0  33247  idomrcanOLD  33251  isdrng4  33264  fracfld  33275  lindssn  33371  lindfpropd  33375  elrspunidl  33421  elrspunsn  33422  drngidl  33426  mxidlmaxv  33461  mxidlirredi  33464  opprqusdrng  33486  qsdrnglem2  33489  rprmcl  33511  rprmirred  33524  pidufd  33536  1arithufdlem3  33539  dfufd2  33543  zringfrac  33547  ply1dg3rt0irred  33572  gsummoncoe1fzo  33583  lindsunlem  33637  fedgmullem1  33642  fedgmullem2  33643  assafld  33650  irngnminplynz  33705  submatminr1  33756  qtophaus  33782  qqhval2  33928  esummono  34018  gsumesum  34023  esum2dlem  34056  measvuni  34178  fiunelcarsg  34281  sitgclg  34307  sitgaddlemb  34313  eulerpartlemsv2  34323  eulerpartlemsv3  34326  eulerpartlemgc  34327  eulerpartlemv  34329  signstfvneq0  34549  signstfvcl  34550  signstfveq0a  34553  signstfveq0  34554  signsvfn  34559  signsvtp  34560  signsvtn  34561  signsvfpn  34562  signsvfnn  34563  signlem0  34564  hgt750leme  34635  iprodgam  35704  poimirlem2  37582  rrndstprj2  37791  lsatelbN  38962  lsatfixedN  38965  lkreqN  39126  lkrlspeqN  39127  dochnel2  41349  dochnel  41350  djhcvat42  41372  dochsnshp  41410  dochexmidat  41416  dochsnkr  41429  dochsnkr2  41430  dochsnkr2cl  41431  dochflcl  41432  dochfl1  41433  dochfln0  41434  lcfl6lem  41455  lcfl7lem  41456  lcfl8b  41461  lclkrlem2a  41464  lclkrlem2b  41465  lclkrlem2c  41466  lclkrlem2d  41467  lclkrlem2e  41468  lclkrlem2f  41469  lcfrlem14  41513  lcfrlem15  41514  lcfrlem16  41515  lcfrlem17  41516  lcfrlem18  41517  lcfrlem19  41518  lcfrlem20  41519  lcfrlem21  41520  lcfrlem23  41522  lcfrlem25  41524  lcfrlem26  41525  lcfrlem35  41534  lcfrlem36  41535  mapdn0  41626  mapdpglem29  41657  mapdpglem24  41661  baerlem3lem1  41664  baerlem5alem1  41665  baerlem5blem1  41666  baerlem3lem2  41667  baerlem5alem2  41668  baerlem5blem2  41669  baerlem5amN  41673  baerlem5bmN  41674  baerlem5abmN  41675  mapdindp0  41676  mapdindp1  41677  mapdindp2  41678  mapdindp3  41679  mapdindp4  41680  mapdheq2  41686  mapdheq4lem  41688  mapdheq4  41689  mapdh6lem1N  41690  mapdh6lem2N  41691  mapdh6aN  41692  mapdh6bN  41694  mapdh6cN  41695  mapdh6dN  41696  mapdh6eN  41697  mapdh6fN  41698  mapdh6gN  41699  mapdh6hN  41700  mapdh6iN  41701  mapdh7eN  41705  mapdh7cN  41706  mapdh7dN  41707  mapdh7fN  41708  mapdh75e  41709  mapdh75fN  41712  hvmaplfl  41724  mapdhvmap  41726  mapdh8aa  41733  mapdh8ab  41734  mapdh8ad  41736  mapdh8b  41737  mapdh8c  41738  mapdh8d0N  41739  mapdh8d  41740  mapdh8e  41741  mapdh9a  41746  mapdh9aOLDN  41747  hdmap1val2  41757  hdmap1eq  41758  hdmap1valc  41760  hdmap1eq2  41762  hdmap1eq4N  41763  hdmap1l6lem1  41764  hdmap1l6lem2  41765  hdmap1l6a  41766  hdmap1l6b  41768  hdmap1l6c  41769  hdmap1l6d  41770  hdmap1l6e  41771  hdmap1l6f  41772  hdmap1l6g  41773  hdmap1l6h  41774  hdmap1l6i  41775  hdmap1eulem  41779  hdmap1eulemOLDN  41780  hdmapcl  41787  hdmapval2lem  41788  hdmapval0  41790  hdmapeveclem  41791  hdmapevec  41792  hdmapval3lemN  41794  hdmapval3N  41795  hdmap10lem  41796  hdmap11lem1  41798  hdmap11lem2  41799  hdmapnzcl  41802  hdmaprnlem3N  41807  hdmaprnlem3uN  41808  hdmaprnlem4N  41810  hdmaprnlem7N  41812  hdmaprnlem8N  41813  hdmaprnlem9N  41814  hdmaprnlem3eN  41815  hdmaprnlem16N  41819  hdmap14lem1  41825  hdmap14lem2N  41826  hdmap14lem3  41827  hdmap14lem4a  41828  hdmap14lem6  41830  hdmap14lem8  41832  hdmap14lem9  41833  hdmap14lem10  41834  hdmap14lem11  41835  hdmap14lem12  41836  hgmaprnlem1N  41853  hgmaprnlem2N  41854  hgmaprnlem3N  41855  hgmaprnlem4N  41856  hdmapip1  41873  hdmapinvlem1  41875  hdmapinvlem2  41876  hdmapinvlem3  41877  hdmapinvlem4  41878  hdmapglem5  41879  hgmapvvlem1  41880  hgmapvvlem2  41881  hgmapvvlem3  41882  hdmapglem7a  41884  hdmapglem7b  41885  hdmapglem7  41886  evl1gprodd  42074  nelsubginvcld  42451  nelsubgcld  42452  nelsubgsubcld  42453  domnexpgn0cl  42478  fidomncyc  42490  prjspnfv01  42579  prjspner01  42580  prjspner1  42581  dffltz  42589  qirropth  42864  rmxyneg  42877  rmxm1  42891  rmxluc  42893  rmxdbl  42896  ltrmxnn0  42906  jm2.19lem1  42946  jm2.23  42953  rmxdiophlem  42972  aomclem2  43012  cantnftermord  43282  inaex  44266  bccm1k  44311  dstregt0  45196  fprodexp  45515  fprodabs2  45516  mccllem  45518  fprodcnlem  45520  climrec  45524  climdivf  45533  islpcn  45560  lptre2pt  45561  0ellimcdiv  45570  reclimc  45574  divlimc  45577  cncficcgt0  45809  dvdivf  45843  stoweidlem34  45955  stoweidlem43  45964  etransclem46  46201  etransclem47  46202  etransclem48  46203  hsphoidmvle2  46506  hsphoidmvle  46507  hoidmvlelem3  46518  hoidmvlelem4  46519  hspdifhsp  46537  readdcnnred  47218  resubcnnred  47219  recnmulnred  47220  cndivrenred  47221