Theorem eldifad 3959

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 394   ∈ wcel 2104   ∖ cdif 3944

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-dif 3950

This theorem is referenced by:  xpdifid  6166  unblem1  9297  cantnflem3  9688  cantnflem4  9689  oef1o  9695  infxpenc  10015  acndom2  10051  ackbij1lem18  10234  infpssrlem3  10302  fin23lem26  10322  fin23lem30  10339  pwfseqlem4a  10658  expclz  14054  symgextf  19326  pmtrfinv  19370  symggen  19379  efgsdmi  19641  efgs1b  19645  efgsp1  19646  efgsres  19647  efgredlemf  19650  efgredlemd  19653  efgredlemc  19654  efgredlem  19656  efgrelexlemb  19659  gsum2d2lem  19882  pgpfac1lem2  19986  pgpfac1lem3a  19987  pgpfac1lem3  19988  pgpfac1lem4  19989  isdrng2  20514  lvecinv  20871  lspsncmp  20874  lspsnne1  20875  lspsnnecom  20877  lspabs2  20878  lspsneu  20881  lspdisjb  20884  lspexch  20887  lspindp1  20891  lvecindp2  20897  lspsolv  20901  lspsnat  20903  lsppratlem1  20905  lsppratlem2  20906  fidomndrnglem  21125  frlmssuvc2  21569  maducoeval2  22362  hauscmplem  23130  1stccnp  23186  imasdsf1olem  24099  rrxmetlem  25155  divcncf  25196  dvrec  25707  dvmptdiv  25726  ftc1lem6  25793  elqaalem1  26068  elqaalem3  26070  ulmdvlem3  26150  abelthlem6  26184  abelthlem7a  26185  abelthlem7  26186  logtayl  26404  dmgmn0  26766  dmgmaddnn0  26767  dmgmdivn0  26768  lgamgulmlem2  26770  lgamgulmlem3  26771  lgamgulmlem5  26773  lgamgulmlem6  26774  lgamgulm2  26776  lgambdd  26777  lgamucov  26778  lgamcvg2  26795  gamcvg  26796  gamcvg2lem  26799  ftalem3  26815  lgsqrlem1  27085  lgsqrlem2  27086  lgsqrlem3  27087  lgsqrlem4  27088  lgseisenlem1  27114  lgseisenlem2  27115  lgseisenlem3  27116  lgseisenlem4  27117  lgseisen  27118  lgsquadlem1  27119  lgsquadlem2  27120  lgsquadlem3  27121  chebbnd1lem1  27208  dchrisum0re  27252  dchrisum0lema  27253  dchrisum0lem1b  27254  dchrisum0lem1  27255  dchrisum0lem2a  27256  dchrisum0lem2  27257  tgisline  28145  elntg  28509  uhgrss  28591  upgrex  28619  edguhgr  28656  1loopgrvd0  29028  disjiunel  32094  suppovss  32173  fvdifsupp  32174  nn0difffzod  32283  gsumhashmul  32478  odpmco  32517  pmtrcnel  32520  pmtrcnelor  32522  cycpmco2f1  32553  cycpmco2rn  32554  cycpmco2lem1  32555  cycpmco2lem2  32556  cycpmco2lem3  32557  cycpmco2lem4  32558  cycpmco2lem5  32559  cycpmco2lem6  32560  cycpmco2lem7  32561  cycpmco2  32562  cyc3co2  32569  tocyccntz  32573  cyc3conja  32586  idomrcan  32647  isdrng4  32665  lindssn  32768  lindfpropd  32772  elrspunidl  32820  elrspunsn  32821  drngidl  32825  mxidlmaxv  32858  mxidlirredi  32861  opprqusdrng  32881  qsdrnglem2  32884  evls1fpws  32920  gsummoncoe1fzo  32943  lindsunlem  32997  fedgmullem1  33002  fedgmullem2  33003  irngnminplynz  33060  submatminr1  33088  qtophaus  33114  qqhval2  33260  esummono  33350  gsumesum  33355  esum2dlem  33388  measvuni  33510  fiunelcarsg  33613  sitgclg  33639  sitgaddlemb  33645  eulerpartlemsv2  33655  eulerpartlemsv3  33658  eulerpartlemgc  33659  eulerpartlemv  33661  signstfvneq0  33881  signstfvcl  33882  signstfveq0a  33885  signstfveq0  33886  signsvfn  33891  signsvtp  33892  signsvtn  33893  signsvfpn  33894  signsvfnn  33895  signlem0  33896  hgt750leme  33968  iprodgam  35016  poimirlem2  36793  rrndstprj2  37002  lsatelbN  38179  lsatfixedN  38182  lkreqN  38343  lkrlspeqN  38344  dochnel2  40566  dochnel  40567  djhcvat42  40589  dochsnshp  40627  dochexmidat  40633  dochsnkr  40646  dochsnkr2  40647  dochsnkr2cl  40648  dochflcl  40649  dochfl1  40650  dochfln0  40651  lcfl6lem  40672  lcfl7lem  40673  lcfl8b  40678  lclkrlem2a  40681  lclkrlem2b  40682  lclkrlem2c  40683  lclkrlem2d  40684  lclkrlem2e  40685  lclkrlem2f  40686  lcfrlem14  40730  lcfrlem15  40731  lcfrlem16  40732  lcfrlem17  40733  lcfrlem18  40734  lcfrlem19  40735  lcfrlem20  40736  lcfrlem21  40737  lcfrlem23  40739  lcfrlem25  40741  lcfrlem26  40742  lcfrlem35  40751  lcfrlem36  40752  mapdn0  40843  mapdpglem29  40874  mapdpglem24  40878  baerlem3lem1  40881  baerlem5alem1  40882  baerlem5blem1  40883  baerlem3lem2  40884  baerlem5alem2  40885  baerlem5blem2  40886  baerlem5amN  40890  baerlem5bmN  40891  baerlem5abmN  40892  mapdindp0  40893  mapdindp1  40894  mapdindp2  40895  mapdindp3  40896  mapdindp4  40897  mapdheq2  40903  mapdheq4lem  40905  mapdheq4  40906  mapdh6lem1N  40907  mapdh6lem2N  40908  mapdh6aN  40909  mapdh6bN  40911  mapdh6cN  40912  mapdh6dN  40913  mapdh6eN  40914  mapdh6fN  40915  mapdh6gN  40916  mapdh6hN  40917  mapdh6iN  40918  mapdh7eN  40922  mapdh7cN  40923  mapdh7dN  40924  mapdh7fN  40925  mapdh75e  40926  mapdh75fN  40929  hvmaplfl  40941  mapdhvmap  40943  mapdh8aa  40950  mapdh8ab  40951  mapdh8ad  40953  mapdh8b  40954  mapdh8c  40955  mapdh8d0N  40956  mapdh8d  40957  mapdh8e  40958  mapdh9a  40963  mapdh9aOLDN  40964  hdmap1val2  40974  hdmap1eq  40975  hdmap1valc  40977  hdmap1eq2  40979  hdmap1eq4N  40980  hdmap1l6lem1  40981  hdmap1l6lem2  40982  hdmap1l6a  40983  hdmap1l6b  40985  hdmap1l6c  40986  hdmap1l6d  40987  hdmap1l6e  40988  hdmap1l6f  40989  hdmap1l6g  40990  hdmap1l6h  40991  hdmap1l6i  40992  hdmap1eulem  40996  hdmap1eulemOLDN  40997  hdmapcl  41004  hdmapval2lem  41005  hdmapval0  41007  hdmapeveclem  41008  hdmapevec  41009  hdmapval3lemN  41011  hdmapval3N  41012  hdmap10lem  41013  hdmap11lem1  41015  hdmap11lem2  41016  hdmapnzcl  41019  hdmaprnlem3N  41024  hdmaprnlem3uN  41025  hdmaprnlem4N  41027  hdmaprnlem7N  41029  hdmaprnlem8N  41030  hdmaprnlem9N  41031  hdmaprnlem3eN  41032  hdmaprnlem16N  41036  hdmap14lem1  41042  hdmap14lem2N  41043  hdmap14lem3  41044  hdmap14lem4a  41045  hdmap14lem6  41047  hdmap14lem8  41049  hdmap14lem9  41050  hdmap14lem10  41051  hdmap14lem11  41052  hdmap14lem12  41053  hgmaprnlem1N  41070  hgmaprnlem2N  41071  hgmaprnlem3N  41072  hgmaprnlem4N  41073  hdmapip1  41090  hdmapinvlem1  41092  hdmapinvlem2  41093  hdmapinvlem3  41094  hdmapinvlem4  41095  hdmapglem5  41096  hgmapvvlem1  41097  hgmapvvlem2  41098  hgmapvvlem3  41099  hdmapglem7a  41101  hdmapglem7b  41102  hdmapglem7  41103  nelsubginvcld  41376  nelsubgcld  41377  nelsubgsubcld  41378  prjspnfv01  41668  prjspner01  41669  prjspner1  41670  dffltz  41678  qirropth  41948  rmxyneg  41961  rmxm1  41975  rmxluc  41977  rmxdbl  41980  ltrmxnn0  41990  jm2.19lem1  42030  jm2.23  42037  rmxdiophlem  42056  aomclem2  42099  cantnftermord  42372  inaex  43358  bccm1k  43403  dstregt0  44289  fprodexp  44608  fprodabs2  44609  mccllem  44611  fprodcnlem  44613  climrec  44617  climdivf  44626  islpcn  44653  lptre2pt  44654  0ellimcdiv  44663  reclimc  44667  divlimc  44670  cncficcgt0  44902  dvdivf  44936  stoweidlem34  45048  stoweidlem43  45057  etransclem46  45294  etransclem47  45295  etransclem48  45296  hsphoidmvle2  45599  hsphoidmvle  45600  hoidmvlelem3  45611  hoidmvlelem4  45612  hspdifhsp  45630  readdcnnred  46309  resubcnnred  46310  recnmulnred  46311  cndivrenred  46312  zrzeroorngc  46988  zrtermoringc  47056  zrninitoringc  47057  nzerooringczr  47058