Theorem eldifad 3919

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   ∈ wcel 2145   ∖ cdif 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-dif 3910

This theorem is referenced by:  xpdifid  6156  xpdifcnvepel  6157  fvdifsupp  8155  unblem1  9240  cantnflem3  9648  cantnflem4  9649  oef1o  9655  infxpenc  9990  acndom2  10026  ackbij1lem18  10207  infpssrlem3  10277  fin23lem26  10297  fin23lem30  10314  pwfseqlem4a  10634  elfzodif0  13787  expclz  14108  pfxchn  18654  chnind  18665  chnccats1  18669  chnccat  18670  symgextf  19475  pmtrfinv  19519  symggen  19528  efgsdmi  19790  efgs1b  19794  efgsp1  19795  efgsres  19796  efgredlemf  19799  efgredlemd  19802  efgredlemc  19803  efgredlem  19805  efgrelexlemb  19808  gsum2d2lem  20031  pgpfac1lem2  20135  pgpfac1lem3a  20136  pgpfac1lem3  20137  pgpfac1lem4  20138  zrzeroorngc  20717  zrtermoringc  20748  zrninitoringc  20749  domneq0r  20796  isdrng2  20815  fidomndrnglem  20842  lvecinv  21203  lspsncmp  21206  lspsnne1  21207  lspsnnecom  21209  lspabs2  21210  lspsneu  21213  lspdisjb  21216  lspexch  21219  lspindp1  21223  lvecindp2  21229  lspsolv  21233  lspsnat  21235  lsppratlem1  21237  lsppratlem2  21238  prmidlsubm  21444  nzerooringczr  21587  frlmssuvc2  21902  evls1fpws  22486  maducoeval2  22754  hauscmplem  23520  1stccnp  23576  imasdsf1olem  24487  rrxmetlem  25523  divcncf  25563  dvrec  26071  dvmptdiv  26090  ftc1lem6  26157  elqaalem1  26437  elqaalem3  26439  ulmdvlem3  26519  abelthlem6  26553  abelthlem7a  26554  abelthlem7  26555  logtayl  26779  dmgmn0  27144  dmgmaddnn0  27145  dmgmdivn0  27146  lgamgulmlem2  27148  lgamgulmlem3  27149  lgamgulmlem5  27151  lgamgulmlem6  27152  lgamgulm2  27154  lgambdd  27155  lgamucov  27156  lgamcvg2  27173  gamcvg  27174  gamcvg2lem  27177  ftalem3  27193  lgsqrlem1  27464  lgsqrlem2  27465  lgsqrlem3  27466  lgsqrlem4  27467  lgseisenlem1  27493  lgseisenlem2  27494  lgseisenlem3  27495  lgseisenlem4  27496  lgseisen  27497  lgsquadlem1  27498  lgsquadlem2  27499  lgsquadlem3  27500  chebbnd1lem1  27587  dchrisum0re  27631  dchrisum0lema  27632  dchrisum0lem1b  27633  dchrisum0lem1  27634  dchrisum0lem2a  27635  dchrisum0lem2  27636  tgisline  28850  tgelrnpln  29002  elplng  29006  elplngid  29008  plngcplem  29011  plngrotlem1  29013  plngrotlem2  29014  plngrotlem3  29015  plngrot  29016  lnssplnglem  29017  lnssplng  29018  elntg  29239  uhgrss  29319  upgrex  29347  edguhgr  29384  1loopgrvd0  29759  disjiunel  32847  suppovss  32934  nn0difffzod  33057  gsumfs2d  33289  gsumhashmul  33295  suppgsumssiun  33300  odpmco  33314  pmtrcnel  33317  pmtrcnelor  33319  cycpmco2f1  33352  cycpmco2rn  33353  cycpmco2lem1  33354  cycpmco2lem2  33355  cycpmco2lem3  33356  cycpmco2lem4  33357  cycpmco2lem5  33358  cycpmco2lem6  33359  cycpmco2lem7  33360  cycpmco2  33361  cyc3co2  33368  tocyccntz  33372  cyc3conja  33385  fxpsdrg  33403  elrgspnlem2  33471  elrgspnlem4  33473  elrgspnsubrunlem2  33476  domnprodn0  33506  domnprodeq0  33507  isdrng4  33526  fracfld  33539  lindssn  33602  lindfpropd  33606  elrspunidl  33647  elrspunsn  33648  drngidl  33652  mxidlmaxv  33663  mxidlirredi  33666  opprqusdrng  33687  qsdrnglem2  33690  dflringlem  33696  dflringlem2  33697  rprmcl  33720  rprmirred  33733  pidufd  33745  1arithufdlem3  33748  dfufd2  33752  zringfrac  33756  deg1prod  33785  ply1dg3rt0irred  33786  gsummoncoe1fzo  33799  mplvrpmrhm  33849  psrgsum  33850  psrmonprod  33854  esplyfval2  33867  lindsunlem  33926  fedgmullem1  33931  fedgmullem2  33932  assafld  33939  fldextrspunlsp  33976  extdgfialglem2  33995  irngnminplynz  34014  constrextdg2lem  34050  constrfiss  34053  constrsdrg  34077  submatminr1  34112  qtophaus  34138  qqhval2  34284  esummono  34356  gsumesum  34361  esum2dlem  34394  measvuni  34516  fiunelcarsg  34618  sitgclg  34644  sitgaddlemb  34650  eulerpartlemsv2  34660  eulerpartlemsv3  34663  eulerpartlemgc  34664  eulerpartlemv  34666  signstfvneq0  34871  signstfvcl  34872  signstfveq0a  34875  signstfveq0  34876  signsvfn  34881  signsvtp  34882  signsvtn  34883  signsvfpn  34884  signsvfnn  34885  signlem0  34886  hgt750leme  34957  onvf1odlem4  35456  iprodgam  36100  ttcwf2  36893  mh-inf3f1  36909  poimirlem2  38128  rrndstprj2  38337  lsatelbN  39637  lsatfixedN  39640  lkreqN  39801  lkrlspeqN  39802  dochnel2  42023  dochnel  42024  djhcvat42  42046  dochsnshp  42084  dochexmidat  42090  dochsnkr  42103  dochsnkr2  42104  dochsnkr2cl  42105  dochflcl  42106  dochfl1  42107  dochfln0  42108  lcfl6lem  42129  lcfl7lem  42130  lcfl8b  42135  lclkrlem2a  42138  lclkrlem2b  42139  lclkrlem2c  42140  lclkrlem2d  42141  lclkrlem2e  42142  lclkrlem2f  42143  lcfrlem14  42187  lcfrlem15  42188  lcfrlem16  42189  lcfrlem17  42190  lcfrlem18  42191  lcfrlem19  42192  lcfrlem20  42193  lcfrlem21  42194  lcfrlem23  42196  lcfrlem25  42198  lcfrlem26  42199  lcfrlem35  42208  lcfrlem36  42209  mapdn0  42300  mapdpglem29  42331  mapdpglem24  42335  baerlem3lem1  42338  baerlem5alem1  42339  baerlem5blem1  42340  baerlem3lem2  42341  baerlem5alem2  42342  baerlem5blem2  42343  baerlem5amN  42347  baerlem5bmN  42348  baerlem5abmN  42349  mapdindp0  42350  mapdindp1  42351  mapdindp2  42352  mapdindp3  42353  mapdindp4  42354  mapdheq2  42360  mapdheq4lem  42362  mapdheq4  42363  mapdh6lem1N  42364  mapdh6lem2N  42365  mapdh6aN  42366  mapdh6bN  42368  mapdh6cN  42369  mapdh6dN  42370  mapdh6eN  42371  mapdh6fN  42372  mapdh6gN  42373  mapdh6hN  42374  mapdh6iN  42375  mapdh7eN  42379  mapdh7cN  42380  mapdh7dN  42381  mapdh7fN  42382  mapdh75e  42383  mapdh75fN  42386  hvmaplfl  42398  mapdhvmap  42400  mapdh8aa  42407  mapdh8ab  42408  mapdh8ad  42410  mapdh8b  42411  mapdh8c  42412  mapdh8d0N  42413  mapdh8d  42414  mapdh8e  42415  mapdh9a  42420  mapdh9aOLDN  42421  hdmap1val2  42431  hdmap1eq  42432  hdmap1valc  42434  hdmap1eq2  42436  hdmap1eq4N  42437  hdmap1l6lem1  42438  hdmap1l6lem2  42439  hdmap1l6a  42440  hdmap1l6b  42442  hdmap1l6c  42443  hdmap1l6d  42444  hdmap1l6e  42445  hdmap1l6f  42446  hdmap1l6g  42447  hdmap1l6h  42448  hdmap1l6i  42449  hdmap1eulem  42453  hdmap1eulemOLDN  42454  hdmapcl  42461  hdmapval2lem  42462  hdmapval0  42464  hdmapeveclem  42465  hdmapevec  42466  hdmapval3lemN  42468  hdmapval3N  42469  hdmap10lem  42470  hdmap11lem1  42472  hdmap11lem2  42473  hdmapnzcl  42476  hdmaprnlem3N  42481  hdmaprnlem3uN  42482  hdmaprnlem4N  42484  hdmaprnlem7N  42486  hdmaprnlem8N  42487  hdmaprnlem9N  42488  hdmaprnlem3eN  42489  hdmaprnlem16N  42493  hdmap14lem1  42499  hdmap14lem2N  42500  hdmap14lem3  42501  hdmap14lem4a  42502  hdmap14lem6  42504  hdmap14lem8  42506  hdmap14lem9  42507  hdmap14lem10  42508  hdmap14lem11  42509  hdmap14lem12  42510  hgmaprnlem1N  42527  hgmaprnlem2N  42528  hgmaprnlem3N  42529  hgmaprnlem4N  42530  hdmapip1  42547  hdmapinvlem1  42549  hdmapinvlem2  42550  hdmapinvlem3  42551  hdmapinvlem4  42552  hdmapglem5  42553  hgmapvvlem1  42554  hgmapvvlem2  42555  hgmapvvlem3  42556  hdmapglem7a  42558  hdmapglem7b  42559  hdmapglem7  42560  evl1gprodd  42741  nelsubginvcld  43125  nelsubgcld  43126  nelsubgsubcld  43127  domnexpgn0cl  43148  fidomncyc  43160  prjspnfv01  43213  prjspner01  43214  prjspner1  43215  dffltz  43223  qirropth  43492  rmxyneg  43504  rmxm1  43518  rmxluc  43520  rmxdbl  43523  ltrmxnn0  43533  jm2.19lem1  43573  jm2.23  43580  rmxdiophlem  43599  aomclem2  43639  cantnftermord  43904  inaex  44866  bccm1k  44911  dstregt0  45860  fprodexp  46169  fprodabs2  46170  mccllem  46172  fprodcnlem  46174  climrec  46178  climdivf  46187  islpcn  46212  lptre2pt  46213  0ellimcdiv  46222  reclimc  46226  divlimc  46229  cncficcgt0  46461  dvdivf  46495  stoweidlem34  46607  stoweidlem43  46616  etransclem46  46853  etransclem47  46854  etransclem48  46855  hsphoidmvle2  47158  hsphoidmvle  47159  hoidmvlelem3  47170  hoidmvlelem4  47171  hspdifhsp  47189  readdcnnred  47896  resubcnnred  47897  recnmulnred  47898  cndivrenred  47899