Theorem eldifad 3929

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-dif 3920

This theorem is referenced by:  xpdifid  6144  fvdifsupp  8153  unblem1  9246  cantnflem3  9651  cantnflem4  9652  oef1o  9658  infxpenc  9978  acndom2  10014  ackbij1lem18  10196  infpssrlem3  10265  fin23lem26  10285  fin23lem30  10302  pwfseqlem4a  10621  expclz  14056  symgextf  19354  pmtrfinv  19398  symggen  19407  efgsdmi  19669  efgs1b  19673  efgsp1  19674  efgsres  19675  efgredlemf  19678  efgredlemd  19681  efgredlemc  19682  efgredlem  19684  efgrelexlemb  19687  gsum2d2lem  19910  pgpfac1lem2  20014  pgpfac1lem3a  20015  pgpfac1lem3  20016  pgpfac1lem4  20017  zrzeroorngc  20560  zrtermoringc  20591  zrninitoringc  20592  domneq0r  20640  isdrng2  20659  fidomndrnglem  20688  lvecinv  21030  lspsncmp  21033  lspsnne1  21034  lspsnnecom  21036  lspabs2  21037  lspsneu  21040  lspdisjb  21043  lspexch  21046  lspindp1  21050  lvecindp2  21056  lspsolv  21060  lspsnat  21062  lsppratlem1  21064  lsppratlem2  21065  nzerooringczr  21397  frlmssuvc2  21711  evls1fpws  22263  maducoeval2  22534  hauscmplem  23300  1stccnp  23356  imasdsf1olem  24268  rrxmetlem  25314  divcncf  25355  dvrec  25866  dvmptdiv  25885  ftc1lem6  25955  elqaalem1  26234  elqaalem3  26236  ulmdvlem3  26318  abelthlem6  26353  abelthlem7a  26354  abelthlem7  26355  logtayl  26576  dmgmn0  26943  dmgmaddnn0  26944  dmgmdivn0  26945  lgamgulmlem2  26947  lgamgulmlem3  26948  lgamgulmlem5  26950  lgamgulmlem6  26951  lgamgulm2  26953  lgambdd  26954  lgamucov  26955  lgamcvg2  26972  gamcvg  26973  gamcvg2lem  26976  ftalem3  26992  lgsqrlem1  27264  lgsqrlem2  27265  lgsqrlem3  27266  lgsqrlem4  27267  lgseisenlem1  27293  lgseisenlem2  27294  lgseisenlem3  27295  lgseisenlem4  27296  lgseisen  27297  lgsquadlem1  27298  lgsquadlem2  27299  lgsquadlem3  27300  chebbnd1lem1  27387  dchrisum0re  27431  dchrisum0lema  27432  dchrisum0lem1b  27433  dchrisum0lem1  27434  dchrisum0lem2a  27435  dchrisum0lem2  27436  tgisline  28561  elntg  28918  uhgrss  28998  upgrex  29026  edguhgr  29063  1loopgrvd0  29439  disjiunel  32532  suppovss  32611  elfzodif0  32724  nn0difffzod  32736  pfxchn  32942  chnind  32944  chnccats1  32948  gsumfs2d  33002  gsumhashmul  33008  odpmco  33050  pmtrcnel  33053  pmtrcnelor  33055  cycpmco2f1  33088  cycpmco2rn  33089  cycpmco2lem1  33090  cycpmco2lem2  33091  cycpmco2lem3  33092  cycpmco2lem4  33093  cycpmco2lem5  33094  cycpmco2lem6  33095  cycpmco2lem7  33096  cycpmco2  33097  cyc3co2  33104  tocyccntz  33108  cyc3conja  33121  elrgspnlem2  33201  elrgspnlem4  33203  elrgspnsubrunlem2  33206  domnprodn0  33233  idomrcanOLD  33239  isdrng4  33252  fracfld  33265  lindssn  33356  lindfpropd  33360  elrspunidl  33406  elrspunsn  33407  drngidl  33411  mxidlmaxv  33446  mxidlirredi  33449  opprqusdrng  33471  qsdrnglem2  33474  rprmcl  33496  rprmirred  33509  pidufd  33521  1arithufdlem3  33524  dfufd2  33528  zringfrac  33532  ply1dg3rt0irred  33558  gsummoncoe1fzo  33570  lindsunlem  33627  fedgmullem1  33632  fedgmullem2  33633  assafld  33640  fldextrspunlsp  33676  irngnminplynz  33709  constrextdg2lem  33745  constrfiss  33748  constrsdrg  33772  submatminr1  33807  qtophaus  33833  qqhval2  33979  esummono  34051  gsumesum  34056  esum2dlem  34089  measvuni  34211  fiunelcarsg  34314  sitgclg  34340  sitgaddlemb  34346  eulerpartlemsv2  34356  eulerpartlemsv3  34359  eulerpartlemgc  34360  eulerpartlemv  34362  signstfvneq0  34570  signstfvcl  34571  signstfveq0a  34574  signstfveq0  34575  signsvfn  34580  signsvtp  34581  signsvtn  34582  signsvfpn  34583  signsvfnn  34584  signlem0  34585  hgt750leme  34656  onvf1odlem4  35100  iprodgam  35736  poimirlem2  37623  rrndstprj2  37832  lsatelbN  39006  lsatfixedN  39009  lkreqN  39170  lkrlspeqN  39171  dochnel2  41393  dochnel  41394  djhcvat42  41416  dochsnshp  41454  dochexmidat  41460  dochsnkr  41473  dochsnkr2  41474  dochsnkr2cl  41475  dochflcl  41476  dochfl1  41477  dochfln0  41478  lcfl6lem  41499  lcfl7lem  41500  lcfl8b  41505  lclkrlem2a  41508  lclkrlem2b  41509  lclkrlem2c  41510  lclkrlem2d  41511  lclkrlem2e  41512  lclkrlem2f  41513  lcfrlem14  41557  lcfrlem15  41558  lcfrlem16  41559  lcfrlem17  41560  lcfrlem18  41561  lcfrlem19  41562  lcfrlem20  41563  lcfrlem21  41564  lcfrlem23  41566  lcfrlem25  41568  lcfrlem26  41569  lcfrlem35  41578  lcfrlem36  41579  mapdn0  41670  mapdpglem29  41701  mapdpglem24  41705  baerlem3lem1  41708  baerlem5alem1  41709  baerlem5blem1  41710  baerlem3lem2  41711  baerlem5alem2  41712  baerlem5blem2  41713  baerlem5amN  41717  baerlem5bmN  41718  baerlem5abmN  41719  mapdindp0  41720  mapdindp1  41721  mapdindp2  41722  mapdindp3  41723  mapdindp4  41724  mapdheq2  41730  mapdheq4lem  41732  mapdheq4  41733  mapdh6lem1N  41734  mapdh6lem2N  41735  mapdh6aN  41736  mapdh6bN  41738  mapdh6cN  41739  mapdh6dN  41740  mapdh6eN  41741  mapdh6fN  41742  mapdh6gN  41743  mapdh6hN  41744  mapdh6iN  41745  mapdh7eN  41749  mapdh7cN  41750  mapdh7dN  41751  mapdh7fN  41752  mapdh75e  41753  mapdh75fN  41756  hvmaplfl  41768  mapdhvmap  41770  mapdh8aa  41777  mapdh8ab  41778  mapdh8ad  41780  mapdh8b  41781  mapdh8c  41782  mapdh8d0N  41783  mapdh8d  41784  mapdh8e  41785  mapdh9a  41790  mapdh9aOLDN  41791  hdmap1val2  41801  hdmap1eq  41802  hdmap1valc  41804  hdmap1eq2  41806  hdmap1eq4N  41807  hdmap1l6lem1  41808  hdmap1l6lem2  41809  hdmap1l6a  41810  hdmap1l6b  41812  hdmap1l6c  41813  hdmap1l6d  41814  hdmap1l6e  41815  hdmap1l6f  41816  hdmap1l6g  41817  hdmap1l6h  41818  hdmap1l6i  41819  hdmap1eulem  41823  hdmap1eulemOLDN  41824  hdmapcl  41831  hdmapval2lem  41832  hdmapval0  41834  hdmapeveclem  41835  hdmapevec  41836  hdmapval3lemN  41838  hdmapval3N  41839  hdmap10lem  41840  hdmap11lem1  41842  hdmap11lem2  41843  hdmapnzcl  41846  hdmaprnlem3N  41851  hdmaprnlem3uN  41852  hdmaprnlem4N  41854  hdmaprnlem7N  41856  hdmaprnlem8N  41857  hdmaprnlem9N  41858  hdmaprnlem3eN  41859  hdmaprnlem16N  41863  hdmap14lem1  41869  hdmap14lem2N  41870  hdmap14lem3  41871  hdmap14lem4a  41872  hdmap14lem6  41874  hdmap14lem8  41876  hdmap14lem9  41877  hdmap14lem10  41878  hdmap14lem11  41879  hdmap14lem12  41880  hgmaprnlem1N  41897  hgmaprnlem2N  41898  hgmaprnlem3N  41899  hgmaprnlem4N  41900  hdmapip1  41917  hdmapinvlem1  41919  hdmapinvlem2  41920  hdmapinvlem3  41921  hdmapinvlem4  41922  hdmapglem5  41923  hgmapvvlem1  41924  hgmapvvlem2  41925  hgmapvvlem3  41926  hdmapglem7a  41928  hdmapglem7b  41929  hdmapglem7  41930  evl1gprodd  42112  nelsubginvcld  42491  nelsubgcld  42492  nelsubgsubcld  42493  domnexpgn0cl  42518  fidomncyc  42530  prjspnfv01  42619  prjspner01  42620  prjspner1  42621  dffltz  42629  qirropth  42903  rmxyneg  42916  rmxm1  42930  rmxluc  42932  rmxdbl  42935  ltrmxnn0  42945  jm2.19lem1  42985  jm2.23  42992  rmxdiophlem  43011  aomclem2  43051  cantnftermord  43316  inaex  44293  bccm1k  44338  dstregt0  45287  fprodexp  45599  fprodabs2  45600  mccllem  45602  fprodcnlem  45604  climrec  45608  climdivf  45617  islpcn  45644  lptre2pt  45645  0ellimcdiv  45654  reclimc  45658  divlimc  45661  cncficcgt0  45893  dvdivf  45927  stoweidlem34  46039  stoweidlem43  46048  etransclem46  46285  etransclem47  46286  etransclem48  46287  hsphoidmvle2  46590  hsphoidmvle  46591  hoidmvlelem3  46602  hoidmvlelem4  46603  hspdifhsp  46621  readdcnnred  47308  resubcnnred  47309  recnmulnred  47310  cndivrenred  47311