Theorem eldifad 3895

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∈ wcel 2119   ∖ cdif 3880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-dif 3886

This theorem is referenced by:  xpdifid  6119  fvdifsupp  8111  unblem1  9192  cantnflem3  9603  cantnflem4  9604  oef1o  9610  infxpenc  9931  acndom2  9967  ackbij1lem18  10149  infpssrlem3  10218  fin23lem26  10238  fin23lem30  10255  pwfseqlem4a  10575  elfzodif0  13716  expclz  14037  pfxchn  18567  chnind  18578  chnccats1  18582  chnccat  18583  symgextf  19383  pmtrfinv  19427  symggen  19436  efgsdmi  19698  efgs1b  19702  efgsp1  19703  efgsres  19704  efgredlemf  19707  efgredlemd  19710  efgredlemc  19711  efgredlem  19713  efgrelexlemb  19716  gsum2d2lem  19939  pgpfac1lem2  20043  pgpfac1lem3a  20044  pgpfac1lem3  20045  pgpfac1lem4  20046  zrzeroorngc  20616  zrtermoringc  20647  zrninitoringc  20648  domneq0r  20696  isdrng2  20715  fidomndrnglem  20744  lvecinv  21106  lspsncmp  21109  lspsnne1  21110  lspsnnecom  21112  lspabs2  21113  lspsneu  21116  lspdisjb  21119  lspexch  21122  lspindp1  21126  lvecindp2  21132  lspsolv  21136  lspsnat  21138  lsppratlem1  21140  lsppratlem2  21141  nzerooringczr  21455  frlmssuvc2  21770  evls1fpws  22355  maducoeval2  22623  hauscmplem  23389  1stccnp  23445  imasdsf1olem  24356  rrxmetlem  25392  divcncf  25432  dvrec  25940  dvmptdiv  25959  ftc1lem6  26026  elqaalem1  26303  elqaalem3  26305  ulmdvlem3  26385  abelthlem6  26419  abelthlem7a  26420  abelthlem7  26421  logtayl  26642  dmgmn0  27007  dmgmaddnn0  27008  dmgmdivn0  27009  lgamgulmlem2  27011  lgamgulmlem3  27012  lgamgulmlem5  27014  lgamgulmlem6  27015  lgamgulm2  27017  lgambdd  27018  lgamucov  27019  lgamcvg2  27036  gamcvg  27037  gamcvg2lem  27040  ftalem3  27056  lgsqrlem1  27327  lgsqrlem2  27328  lgsqrlem3  27329  lgsqrlem4  27330  lgseisenlem1  27356  lgseisenlem2  27357  lgseisenlem3  27358  lgseisenlem4  27359  lgseisen  27360  lgsquadlem1  27361  lgsquadlem2  27362  lgsquadlem3  27363  chebbnd1lem1  27450  dchrisum0re  27494  dchrisum0lema  27495  dchrisum0lem1b  27496  dchrisum0lem1  27497  dchrisum0lem2a  27498  dchrisum0lem2  27499  tgisline  28713  elntg  29071  uhgrss  29151  upgrex  29179  edguhgr  29216  1loopgrvd0  29591  disjiunel  32685  suppovss  32773  nn0difffzod  32896  gsumfs2d  33142  gsumhashmul  33148  suppgsumssiun  33153  odpmco  33167  pmtrcnel  33170  pmtrcnelor  33172  cycpmco2f1  33205  cycpmco2rn  33206  cycpmco2lem1  33207  cycpmco2lem2  33208  cycpmco2lem3  33209  cycpmco2lem4  33210  cycpmco2lem5  33211  cycpmco2lem6  33212  cycpmco2lem7  33213  cycpmco2  33214  cyc3co2  33221  tocyccntz  33225  cyc3conja  33238  fxpsdrg  33256  elrgspnlem2  33324  elrgspnlem4  33326  elrgspnsubrunlem2  33329  domnprodn0  33356  domnprodeq0  33357  idomrcanOLD  33363  isdrng4  33379  fracfld  33392  lindssn  33461  lindfpropd  33465  elrspunidl  33511  elrspunsn  33512  drngidl  33516  mxidlmaxv  33551  mxidlirredi  33554  opprqusdrng  33576  qsdrnglem2  33579  rprmcl  33601  rprmirred  33614  pidufd  33626  1arithufdlem3  33629  dfufd2  33633  zringfrac  33637  deg1prod  33666  ply1dg3rt0irred  33667  gsummoncoe1fzo  33680  mplvrpmrhm  33731  psrgsum  33732  psrmonprod  33736  esplyfval2  33749  lindsunlem  33808  fedgmullem1  33813  fedgmullem2  33814  assafld  33821  fldextrspunlsp  33858  extdgfialglem2  33877  irngnminplynz  33896  constrextdg2lem  33932  constrfiss  33935  constrsdrg  33959  submatminr1  33994  qtophaus  34020  qqhval2  34166  esummono  34238  gsumesum  34243  esum2dlem  34276  measvuni  34398  fiunelcarsg  34500  sitgclg  34526  sitgaddlemb  34532  eulerpartlemsv2  34542  eulerpartlemsv3  34545  eulerpartlemgc  34546  eulerpartlemv  34548  signstfvneq0  34756  signstfvcl  34757  signstfveq0a  34760  signstfveq0  34761  signsvfn  34766  signsvtp  34767  signsvtn  34768  signsvfpn  34769  signsvfnn  34770  signlem0  34771  hgt750leme  34842  onvf1odlem4  35334  iprodgam  35970  ttcwf2  36753  mh-inf3f1  36769  poimirlem2  37989  rrndstprj2  38198  lsatelbN  39498  lsatfixedN  39501  lkreqN  39662  lkrlspeqN  39663  dochnel2  41884  dochnel  41885  djhcvat42  41907  dochsnshp  41945  dochexmidat  41951  dochsnkr  41964  dochsnkr2  41965  dochsnkr2cl  41966  dochflcl  41967  dochfl1  41968  dochfln0  41969  lcfl6lem  41990  lcfl7lem  41991  lcfl8b  41996  lclkrlem2a  41999  lclkrlem2b  42000  lclkrlem2c  42001  lclkrlem2d  42002  lclkrlem2e  42003  lclkrlem2f  42004  lcfrlem14  42048  lcfrlem15  42049  lcfrlem16  42050  lcfrlem17  42051  lcfrlem18  42052  lcfrlem19  42053  lcfrlem20  42054  lcfrlem21  42055  lcfrlem23  42057  lcfrlem25  42059  lcfrlem26  42060  lcfrlem35  42069  lcfrlem36  42070  mapdn0  42161  mapdpglem29  42192  mapdpglem24  42196  baerlem3lem1  42199  baerlem5alem1  42200  baerlem5blem1  42201  baerlem3lem2  42202  baerlem5alem2  42203  baerlem5blem2  42204  baerlem5amN  42208  baerlem5bmN  42209  baerlem5abmN  42210  mapdindp0  42211  mapdindp1  42212  mapdindp2  42213  mapdindp3  42214  mapdindp4  42215  mapdheq2  42221  mapdheq4lem  42223  mapdheq4  42224  mapdh6lem1N  42225  mapdh6lem2N  42226  mapdh6aN  42227  mapdh6bN  42229  mapdh6cN  42230  mapdh6dN  42231  mapdh6eN  42232  mapdh6fN  42233  mapdh6gN  42234  mapdh6hN  42235  mapdh6iN  42236  mapdh7eN  42240  mapdh7cN  42241  mapdh7dN  42242  mapdh7fN  42243  mapdh75e  42244  mapdh75fN  42247  hvmaplfl  42259  mapdhvmap  42261  mapdh8aa  42268  mapdh8ab  42269  mapdh8ad  42271  mapdh8b  42272  mapdh8c  42273  mapdh8d0N  42274  mapdh8d  42275  mapdh8e  42276  mapdh9a  42281  mapdh9aOLDN  42282  hdmap1val2  42292  hdmap1eq  42293  hdmap1valc  42295  hdmap1eq2  42297  hdmap1eq4N  42298  hdmap1l6lem1  42299  hdmap1l6lem2  42300  hdmap1l6a  42301  hdmap1l6b  42303  hdmap1l6c  42304  hdmap1l6d  42305  hdmap1l6e  42306  hdmap1l6f  42307  hdmap1l6g  42308  hdmap1l6h  42309  hdmap1l6i  42310  hdmap1eulem  42314  hdmap1eulemOLDN  42315  hdmapcl  42322  hdmapval2lem  42323  hdmapval0  42325  hdmapeveclem  42326  hdmapevec  42327  hdmapval3lemN  42329  hdmapval3N  42330  hdmap10lem  42331  hdmap11lem1  42333  hdmap11lem2  42334  hdmapnzcl  42337  hdmaprnlem3N  42342  hdmaprnlem3uN  42343  hdmaprnlem4N  42345  hdmaprnlem7N  42347  hdmaprnlem8N  42348  hdmaprnlem9N  42349  hdmaprnlem3eN  42350  hdmaprnlem16N  42354  hdmap14lem1  42360  hdmap14lem2N  42361  hdmap14lem3  42362  hdmap14lem4a  42363  hdmap14lem6  42365  hdmap14lem8  42367  hdmap14lem9  42368  hdmap14lem10  42369  hdmap14lem11  42370  hdmap14lem12  42371  hgmaprnlem1N  42388  hgmaprnlem2N  42389  hgmaprnlem3N  42390  hgmaprnlem4N  42391  hdmapip1  42408  hdmapinvlem1  42410  hdmapinvlem2  42411  hdmapinvlem3  42412  hdmapinvlem4  42413  hdmapglem5  42414  hgmapvvlem1  42415  hgmapvvlem2  42416  hgmapvvlem3  42417  hdmapglem7a  42419  hdmapglem7b  42420  hdmapglem7  42421  evl1gprodd  42602  nelsubginvcld  42986  nelsubgcld  42987  nelsubgsubcld  42988  domnexpgn0cl  43009  fidomncyc  43021  prjspnfv01  43074  prjspner01  43075  prjspner1  43076  dffltz  43084  qirropth  43353  rmxyneg  43365  rmxm1  43379  rmxluc  43381  rmxdbl  43384  ltrmxnn0  43394  jm2.19lem1  43434  jm2.23  43441  rmxdiophlem  43460  aomclem2  43500  cantnftermord  43765  inaex  44741  bccm1k  44786  dstregt0  45730  fprodexp  46039  fprodabs2  46040  mccllem  46042  fprodcnlem  46044  climrec  46048  climdivf  46057  islpcn  46082  lptre2pt  46083  0ellimcdiv  46092  reclimc  46096  divlimc  46099  cncficcgt0  46331  dvdivf  46365  stoweidlem34  46477  stoweidlem43  46486  etransclem46  46723  etransclem47  46724  etransclem48  46725  hsphoidmvle2  47028  hsphoidmvle  47029  hoidmvlelem3  47040  hoidmvlelem4  47041  hspdifhsp  47059  readdcnnred  47766  resubcnnred  47767  recnmulnred  47768  cndivrenred  47769