Theorem eldifad 3893

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∈ wcel 2111   ∖ cdif 3878

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-dif 3884

This theorem is referenced by:  xpdifid  5992  unblem1  8754  cantnflem3  9138  cantnflem4  9139  oef1o  9145  infxpenc  9429  acndom2  9465  ackbij1lem18  9648  infpssrlem3  9716  fin23lem26  9736  fin23lem30  9753  pwfseqlem4a  10072  expclz  13450  symgextf  18537  pmtrfinv  18581  symggen  18590  efgsdmi  18850  efgs1b  18854  efgsp1  18855  efgsres  18856  efgredlemf  18859  efgredlemd  18862  efgredlemc  18863  efgredlem  18865  efgrelexlemb  18868  gsum2d2lem  19086  pgpfac1lem2  19190  pgpfac1lem3a  19191  pgpfac1lem3  19192  pgpfac1lem4  19193  isdrng2  19505  lvecinv  19878  lspsncmp  19881  lspsnne1  19882  lspsnnecom  19884  lspabs2  19885  lspsneu  19888  lspdisjb  19891  lspexch  19894  lspindp1  19898  lvecindp2  19904  lspsolv  19908  lspsnat  19910  lsppratlem1  19912  lsppratlem2  19913  fidomndrnglem  20072  frlmssuvc2  20484  maducoeval2  21245  hauscmplem  22011  1stccnp  22067  imasdsf1olem  22980  rrxmetlem  24011  divcncf  24051  dvrec  24558  dvmptdiv  24577  ftc1lem6  24644  elqaalem1  24915  elqaalem3  24917  ulmdvlem3  24997  abelthlem6  25031  abelthlem7a  25032  abelthlem7  25033  logtayl  25251  dmgmn0  25611  dmgmaddnn0  25612  dmgmdivn0  25613  lgamgulmlem2  25615  lgamgulmlem3  25616  lgamgulmlem5  25618  lgamgulmlem6  25619  lgamgulm2  25621  lgambdd  25622  lgamucov  25623  lgamcvg2  25640  gamcvg  25641  gamcvg2lem  25644  ftalem3  25660  lgsqrlem1  25930  lgsqrlem2  25931  lgsqrlem3  25932  lgsqrlem4  25933  lgseisenlem1  25959  lgseisenlem2  25960  lgseisenlem3  25961  lgseisenlem4  25962  lgseisen  25963  lgsquadlem1  25964  lgsquadlem2  25965  lgsquadlem3  25966  chebbnd1lem1  26053  dchrisum0re  26097  dchrisum0lema  26098  dchrisum0lem1b  26099  dchrisum0lem1  26100  dchrisum0lem2a  26101  dchrisum0lem2  26102  tgisline  26421  elntg  26778  uhgrss  26857  upgrex  26885  edguhgr  26922  1loopgrvd0  27294  disjiunel  30359  suppovss  30443  fvdifsupp  30444  gsumhashmul  30741  odpmco  30780  pmtrcnel  30783  pmtrcnelor  30785  cycpmco2f1  30816  cycpmco2rn  30817  cycpmco2lem1  30818  cycpmco2lem2  30819  cycpmco2lem3  30820  cycpmco2lem4  30821  cycpmco2lem5  30822  cycpmco2lem6  30823  cycpmco2lem7  30824  cycpmco2  30825  cyc3co2  30832  tocyccntz  30836  cyc3conja  30849  lindssn  30993  lindfpropd  30996  elrspunidl  31014  lindsunlem  31108  fedgmullem1  31113  fedgmullem2  31114  submatminr1  31163  qtophaus  31189  qqhval2  31333  esummono  31423  gsumesum  31428  esum2dlem  31461  measvuni  31583  fiunelcarsg  31684  sitgclg  31710  sitgaddlemb  31716  eulerpartlemsv2  31726  eulerpartlemsv3  31729  eulerpartlemgc  31730  eulerpartlemv  31732  signstfvneq0  31952  signstfvcl  31953  signstfveq0a  31956  signstfveq0  31957  signsvfn  31962  signsvtp  31963  signsvtn  31964  signsvfpn  31965  signsvfnn  31966  signlem0  31967  hgt750leme  32039  iprodgam  33087  poimirlem2  35059  rrndstprj2  35269  lsatelbN  36302  lsatfixedN  36305  lkreqN  36466  lkrlspeqN  36467  dochnel2  38688  dochnel  38689  djhcvat42  38711  dochsnshp  38749  dochexmidat  38755  dochsnkr  38768  dochsnkr2  38769  dochsnkr2cl  38770  dochflcl  38771  dochfl1  38772  dochfln0  38773  lcfl6lem  38794  lcfl7lem  38795  lcfl8b  38800  lclkrlem2a  38803  lclkrlem2b  38804  lclkrlem2c  38805  lclkrlem2d  38806  lclkrlem2e  38807  lclkrlem2f  38808  lcfrlem14  38852  lcfrlem15  38853  lcfrlem16  38854  lcfrlem17  38855  lcfrlem18  38856  lcfrlem19  38857  lcfrlem20  38858  lcfrlem21  38859  lcfrlem23  38861  lcfrlem25  38863  lcfrlem26  38864  lcfrlem35  38873  lcfrlem36  38874  mapdn0  38965  mapdpglem29  38996  mapdpglem24  39000  baerlem3lem1  39003  baerlem5alem1  39004  baerlem5blem1  39005  baerlem3lem2  39006  baerlem5alem2  39007  baerlem5blem2  39008  baerlem5amN  39012  baerlem5bmN  39013  baerlem5abmN  39014  mapdindp0  39015  mapdindp1  39016  mapdindp2  39017  mapdindp3  39018  mapdindp4  39019  mapdheq2  39025  mapdheq4lem  39027  mapdheq4  39028  mapdh6lem1N  39029  mapdh6lem2N  39030  mapdh6aN  39031  mapdh6bN  39033  mapdh6cN  39034  mapdh6dN  39035  mapdh6eN  39036  mapdh6fN  39037  mapdh6gN  39038  mapdh6hN  39039  mapdh6iN  39040  mapdh7eN  39044  mapdh7cN  39045  mapdh7dN  39046  mapdh7fN  39047  mapdh75e  39048  mapdh75fN  39051  hvmaplfl  39063  mapdhvmap  39065  mapdh8aa  39072  mapdh8ab  39073  mapdh8ad  39075  mapdh8b  39076  mapdh8c  39077  mapdh8d0N  39078  mapdh8d  39079  mapdh8e  39080  mapdh9a  39085  mapdh9aOLDN  39086  hdmap1val2  39096  hdmap1eq  39097  hdmap1valc  39099  hdmap1eq2  39101  hdmap1eq4N  39102  hdmap1l6lem1  39103  hdmap1l6lem2  39104  hdmap1l6a  39105  hdmap1l6b  39107  hdmap1l6c  39108  hdmap1l6d  39109  hdmap1l6e  39110  hdmap1l6f  39111  hdmap1l6g  39112  hdmap1l6h  39113  hdmap1l6i  39114  hdmap1eulem  39118  hdmap1eulemOLDN  39119  hdmapcl  39126  hdmapval2lem  39127  hdmapval0  39129  hdmapeveclem  39130  hdmapevec  39131  hdmapval3lemN  39133  hdmapval3N  39134  hdmap10lem  39135  hdmap11lem1  39137  hdmap11lem2  39138  hdmapnzcl  39141  hdmaprnlem3N  39146  hdmaprnlem3uN  39147  hdmaprnlem4N  39149  hdmaprnlem7N  39151  hdmaprnlem8N  39152  hdmaprnlem9N  39153  hdmaprnlem3eN  39154  hdmaprnlem16N  39158  hdmap14lem1  39164  hdmap14lem2N  39165  hdmap14lem3  39166  hdmap14lem4a  39167  hdmap14lem6  39169  hdmap14lem8  39171  hdmap14lem9  39172  hdmap14lem10  39173  hdmap14lem11  39174  hdmap14lem12  39175  hgmaprnlem1N  39192  hgmaprnlem2N  39193  hgmaprnlem3N  39194  hgmaprnlem4N  39195  hdmapip1  39212  hdmapinvlem1  39214  hdmapinvlem2  39215  hdmapinvlem3  39216  hdmapinvlem4  39217  hdmapglem5  39218  hgmapvvlem1  39219  hgmapvvlem2  39220  hgmapvvlem3  39221  hdmapglem7a  39223  hdmapglem7b  39224  hdmapglem7  39225  nelsubginvcld  39423  nelsubgcld  39424  nelsubgsubcld  39425  dffltz  39615  qirropth  39849  rmxyneg  39861  rmxm1  39875  rmxluc  39877  rmxdbl  39880  ltrmxnn0  39890  jm2.19lem1  39930  jm2.23  39937  rmxdiophlem  39956  aomclem2  39999  inaex  41005  bccm1k  41046  dstregt0  41912  fprodexp  42236  fprodabs2  42237  mccllem  42239  fprodcnlem  42241  climrec  42245  climdivf  42254  islpcn  42281  lptre2pt  42282  0ellimcdiv  42291  reclimc  42295  divlimc  42298  cncficcgt0  42530  dvdivf  42564  stoweidlem34  42676  stoweidlem43  42685  etransclem46  42922  etransclem47  42923  etransclem48  42924  hsphoidmvle2  43224  hsphoidmvle  43225  hoidmvlelem3  43236  hoidmvlelem4  43237  hspdifhsp  43255  readdcnnred  43860  resubcnnred  43861  recnmulnred  43862  cndivrenred  43863  zrzeroorngc  44626  zrtermoringc  44694  zrninitoringc  44695  nzerooringczr  44696