Theorem eldifad 3948

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   ∈ wcel 2114   ∖ cdif 3933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-dif 3939

This theorem is referenced by:  xpdifid  6025  unblem1  8770  cantnflem3  9154  cantnflem4  9155  oef1o  9161  infxpenc  9444  acndom2  9480  ackbij1lem18  9659  infpssrlem3  9727  fin23lem26  9747  fin23lem30  9764  pwfseqlem4a  10083  expclz  13455  symgextf  18545  pmtrfinv  18589  symggen  18598  efgsdmi  18858  efgs1b  18862  efgsp1  18863  efgsres  18864  efgredlemf  18867  efgredlemd  18870  efgredlemc  18871  efgredlem  18873  efgrelexlemb  18876  gsum2d2lem  19093  pgpfac1lem2  19197  pgpfac1lem3a  19198  pgpfac1lem3  19199  pgpfac1lem4  19200  isdrng2  19512  lvecinv  19885  lspsncmp  19888  lspsnne1  19889  lspsnnecom  19891  lspabs2  19892  lspsneu  19895  lspdisjb  19898  lspexch  19901  lspindp1  19905  lvecindp2  19911  lspsolv  19915  lspsnat  19917  lsppratlem1  19919  lsppratlem2  19920  fidomndrnglem  20079  frlmssuvc2  20939  maducoeval2  21249  hauscmplem  22014  1stccnp  22070  imasdsf1olem  22983  rrxmetlem  24010  divcncf  24048  dvrec  24552  dvmptdiv  24571  ftc1lem6  24638  elqaalem1  24908  elqaalem3  24910  ulmdvlem3  24990  abelthlem6  25024  abelthlem7a  25025  abelthlem7  25026  logtayl  25243  dmgmn0  25603  dmgmaddnn0  25604  dmgmdivn0  25605  lgamgulmlem2  25607  lgamgulmlem3  25608  lgamgulmlem5  25610  lgamgulmlem6  25611  lgamgulm2  25613  lgambdd  25614  lgamucov  25615  lgamcvg2  25632  gamcvg  25633  gamcvg2lem  25636  ftalem3  25652  lgsqrlem1  25922  lgsqrlem2  25923  lgsqrlem3  25924  lgsqrlem4  25925  lgseisenlem1  25951  lgseisenlem2  25952  lgseisenlem3  25953  lgseisenlem4  25954  lgseisen  25955  lgsquadlem1  25956  lgsquadlem2  25957  lgsquadlem3  25958  chebbnd1lem1  26045  dchrisum0re  26089  dchrisum0lema  26090  dchrisum0lem1b  26091  dchrisum0lem1  26092  dchrisum0lem2a  26093  dchrisum0lem2  26094  tgisline  26413  elntg  26770  uhgrss  26849  upgrex  26877  edguhgr  26914  1loopgrvd0  27286  disjiunel  30346  suppovss  30426  fvdifsupp  30427  odpmco  30730  pmtrcnel  30733  pmtrcnelor  30735  cycpmco2f1  30766  cycpmco2rn  30767  cycpmco2lem1  30768  cycpmco2lem2  30769  cycpmco2lem3  30770  cycpmco2lem4  30771  cycpmco2lem5  30772  cycpmco2lem6  30773  cycpmco2lem7  30774  cycpmco2  30775  cyc3co2  30782  tocyccntz  30786  cyc3conja  30799  lindssn  30939  lindfpropd  30942  lindsunlem  31020  fedgmullem1  31025  fedgmullem2  31026  submatminr1  31075  qtophaus  31100  qqhval2  31223  esummono  31313  gsumesum  31318  esum2dlem  31351  measvuni  31473  fiunelcarsg  31574  sitgclg  31600  sitgaddlemb  31606  eulerpartlemsv2  31616  eulerpartlemsv3  31619  eulerpartlemgc  31620  eulerpartlemv  31622  signstfvneq0  31842  signstfvcl  31843  signstfveq0a  31846  signstfveq0  31847  signsvfn  31852  signsvtp  31853  signsvtn  31854  signsvfpn  31855  signsvfnn  31856  signlem0  31857  hgt750leme  31929  iprodgam  32974  poimirlem2  34909  rrndstprj2  35124  lsatelbN  36157  lsatfixedN  36160  lkreqN  36321  lkrlspeqN  36322  dochnel2  38543  dochnel  38544  djhcvat42  38566  dochsnshp  38604  dochexmidat  38610  dochsnkr  38623  dochsnkr2  38624  dochsnkr2cl  38625  dochflcl  38626  dochfl1  38627  dochfln0  38628  lcfl6lem  38649  lcfl7lem  38650  lcfl8b  38655  lclkrlem2a  38658  lclkrlem2b  38659  lclkrlem2c  38660  lclkrlem2d  38661  lclkrlem2e  38662  lclkrlem2f  38663  lcfrlem14  38707  lcfrlem15  38708  lcfrlem16  38709  lcfrlem17  38710  lcfrlem18  38711  lcfrlem19  38712  lcfrlem20  38713  lcfrlem21  38714  lcfrlem23  38716  lcfrlem25  38718  lcfrlem26  38719  lcfrlem35  38728  lcfrlem36  38729  mapdn0  38820  mapdpglem29  38851  mapdpglem24  38855  baerlem3lem1  38858  baerlem5alem1  38859  baerlem5blem1  38860  baerlem3lem2  38861  baerlem5alem2  38862  baerlem5blem2  38863  baerlem5amN  38867  baerlem5bmN  38868  baerlem5abmN  38869  mapdindp0  38870  mapdindp1  38871  mapdindp2  38872  mapdindp3  38873  mapdindp4  38874  mapdheq2  38880  mapdheq4lem  38882  mapdheq4  38883  mapdh6lem1N  38884  mapdh6lem2N  38885  mapdh6aN  38886  mapdh6bN  38888  mapdh6cN  38889  mapdh6dN  38890  mapdh6eN  38891  mapdh6fN  38892  mapdh6gN  38893  mapdh6hN  38894  mapdh6iN  38895  mapdh7eN  38899  mapdh7cN  38900  mapdh7dN  38901  mapdh7fN  38902  mapdh75e  38903  mapdh75fN  38906  hvmaplfl  38918  mapdhvmap  38920  mapdh8aa  38927  mapdh8ab  38928  mapdh8ad  38930  mapdh8b  38931  mapdh8c  38932  mapdh8d0N  38933  mapdh8d  38934  mapdh8e  38935  mapdh9a  38940  mapdh9aOLDN  38941  hdmap1val2  38951  hdmap1eq  38952  hdmap1valc  38954  hdmap1eq2  38956  hdmap1eq4N  38957  hdmap1l6lem1  38958  hdmap1l6lem2  38959  hdmap1l6a  38960  hdmap1l6b  38962  hdmap1l6c  38963  hdmap1l6d  38964  hdmap1l6e  38965  hdmap1l6f  38966  hdmap1l6g  38967  hdmap1l6h  38968  hdmap1l6i  38969  hdmap1eulem  38973  hdmap1eulemOLDN  38974  hdmapcl  38981  hdmapval2lem  38982  hdmapval0  38984  hdmapeveclem  38985  hdmapevec  38986  hdmapval3lemN  38988  hdmapval3N  38989  hdmap10lem  38990  hdmap11lem1  38992  hdmap11lem2  38993  hdmapnzcl  38996  hdmaprnlem3N  39001  hdmaprnlem3uN  39002  hdmaprnlem4N  39004  hdmaprnlem7N  39006  hdmaprnlem8N  39007  hdmaprnlem9N  39008  hdmaprnlem3eN  39009  hdmaprnlem16N  39013  hdmap14lem1  39019  hdmap14lem2N  39020  hdmap14lem3  39021  hdmap14lem4a  39022  hdmap14lem6  39024  hdmap14lem8  39026  hdmap14lem9  39027  hdmap14lem10  39028  hdmap14lem11  39029  hdmap14lem12  39030  hgmaprnlem1N  39047  hgmaprnlem2N  39048  hgmaprnlem3N  39049  hgmaprnlem4N  39050  hdmapip1  39067  hdmapinvlem1  39069  hdmapinvlem2  39070  hdmapinvlem3  39071  hdmapinvlem4  39072  hdmapglem5  39073  hgmapvvlem1  39074  hgmapvvlem2  39075  hgmapvvlem3  39076  hdmapglem7a  39078  hdmapglem7b  39079  hdmapglem7  39080  nelsubginvcld  39177  nelsubgcld  39178  nelsubgsubcld  39179  dffltz  39320  qirropth  39554  rmxyneg  39566  rmxm1  39580  rmxluc  39582  rmxdbl  39585  ltrmxnn0  39595  jm2.19lem1  39635  jm2.23  39642  rmxdiophlem  39661  aomclem2  39704  inaex  40682  bccm1k  40723  dstregt0  41596  fprodexp  41924  fprodabs2  41925  mccllem  41927  fprodcnlem  41929  climrec  41933  climdivf  41942  islpcn  41969  lptre2pt  41970  0ellimcdiv  41979  reclimc  41983  divlimc  41986  cncficcgt0  42220  dvdivf  42256  stoweidlem34  42368  stoweidlem43  42377  etransclem46  42614  etransclem47  42615  etransclem48  42616  hsphoidmvle2  42916  hsphoidmvle  42917  hoidmvlelem3  42928  hoidmvlelem4  42929  hspdifhsp  42947  readdcnnred  43552  resubcnnred  43553  recnmulnred  43554  cndivrenred  43555  zrzeroorngc  44322  zrtermoringc  44390  zrninitoringc  44391  nzerooringczr  44392