Theorem eldifad 3900

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-dif 3891

This theorem is referenced by:  xpdifid  6076  unblem1  9075  cantnflem3  9458  cantnflem4  9459  oef1o  9465  infxpenc  9783  acndom2  9819  ackbij1lem18  10002  infpssrlem3  10070  fin23lem26  10090  fin23lem30  10107  pwfseqlem4a  10426  expclz  13816  symgextf  19034  pmtrfinv  19078  symggen  19087  efgsdmi  19347  efgs1b  19351  efgsp1  19352  efgsres  19353  efgredlemf  19356  efgredlemd  19359  efgredlemc  19360  efgredlem  19362  efgrelexlemb  19365  gsum2d2lem  19583  pgpfac1lem2  19687  pgpfac1lem3a  19688  pgpfac1lem3  19689  pgpfac1lem4  19690  isdrng2  20010  lvecinv  20384  lspsncmp  20387  lspsnne1  20388  lspsnnecom  20390  lspabs2  20391  lspsneu  20394  lspdisjb  20397  lspexch  20400  lspindp1  20404  lvecindp2  20410  lspsolv  20414  lspsnat  20416  lsppratlem1  20418  lsppratlem2  20419  fidomndrnglem  20587  frlmssuvc2  21011  maducoeval2  21798  hauscmplem  22566  1stccnp  22622  imasdsf1olem  23535  rrxmetlem  24580  divcncf  24620  dvrec  25128  dvmptdiv  25147  ftc1lem6  25214  elqaalem1  25488  elqaalem3  25490  ulmdvlem3  25570  abelthlem6  25604  abelthlem7a  25605  abelthlem7  25606  logtayl  25824  dmgmn0  26184  dmgmaddnn0  26185  dmgmdivn0  26186  lgamgulmlem2  26188  lgamgulmlem3  26189  lgamgulmlem5  26191  lgamgulmlem6  26192  lgamgulm2  26194  lgambdd  26195  lgamucov  26196  lgamcvg2  26213  gamcvg  26214  gamcvg2lem  26217  ftalem3  26233  lgsqrlem1  26503  lgsqrlem2  26504  lgsqrlem3  26505  lgsqrlem4  26506  lgseisenlem1  26532  lgseisenlem2  26533  lgseisenlem3  26534  lgseisenlem4  26535  lgseisen  26536  lgsquadlem1  26537  lgsquadlem2  26538  lgsquadlem3  26539  chebbnd1lem1  26626  dchrisum0re  26670  dchrisum0lema  26671  dchrisum0lem1b  26672  dchrisum0lem1  26673  dchrisum0lem2a  26674  dchrisum0lem2  26675  tgisline  26997  elntg  27361  uhgrss  27443  upgrex  27471  edguhgr  27508  1loopgrvd0  27880  disjiunel  30944  suppovss  31026  fvdifsupp  31027  gsumhashmul  31325  odpmco  31364  pmtrcnel  31367  pmtrcnelor  31369  cycpmco2f1  31400  cycpmco2rn  31401  cycpmco2lem1  31402  cycpmco2lem2  31403  cycpmco2lem3  31404  cycpmco2lem4  31405  cycpmco2lem5  31406  cycpmco2lem6  31407  cycpmco2lem7  31408  cycpmco2  31409  cyc3co2  31416  tocyccntz  31420  cyc3conja  31433  lindssn  31582  lindfpropd  31585  elrspunidl  31615  lindsunlem  31714  fedgmullem1  31719  fedgmullem2  31720  submatminr1  31769  qtophaus  31795  qqhval2  31941  esummono  32031  gsumesum  32036  esum2dlem  32069  measvuni  32191  fiunelcarsg  32292  sitgclg  32318  sitgaddlemb  32324  eulerpartlemsv2  32334  eulerpartlemsv3  32337  eulerpartlemgc  32338  eulerpartlemv  32340  signstfvneq0  32560  signstfvcl  32561  signstfveq0a  32564  signstfveq0  32565  signsvfn  32570  signsvtp  32571  signsvtn  32572  signsvfpn  32573  signsvfnn  32574  signlem0  32575  hgt750leme  32647  iprodgam  33717  poimirlem2  35788  rrndstprj2  35998  lsatelbN  37027  lsatfixedN  37030  lkreqN  37191  lkrlspeqN  37192  dochnel2  39413  dochnel  39414  djhcvat42  39436  dochsnshp  39474  dochexmidat  39480  dochsnkr  39493  dochsnkr2  39494  dochsnkr2cl  39495  dochflcl  39496  dochfl1  39497  dochfln0  39498  lcfl6lem  39519  lcfl7lem  39520  lcfl8b  39525  lclkrlem2a  39528  lclkrlem2b  39529  lclkrlem2c  39530  lclkrlem2d  39531  lclkrlem2e  39532  lclkrlem2f  39533  lcfrlem14  39577  lcfrlem15  39578  lcfrlem16  39579  lcfrlem17  39580  lcfrlem18  39581  lcfrlem19  39582  lcfrlem20  39583  lcfrlem21  39584  lcfrlem23  39586  lcfrlem25  39588  lcfrlem26  39589  lcfrlem35  39598  lcfrlem36  39599  mapdn0  39690  mapdpglem29  39721  mapdpglem24  39725  baerlem3lem1  39728  baerlem5alem1  39729  baerlem5blem1  39730  baerlem3lem2  39731  baerlem5alem2  39732  baerlem5blem2  39733  baerlem5amN  39737  baerlem5bmN  39738  baerlem5abmN  39739  mapdindp0  39740  mapdindp1  39741  mapdindp2  39742  mapdindp3  39743  mapdindp4  39744  mapdheq2  39750  mapdheq4lem  39752  mapdheq4  39753  mapdh6lem1N  39754  mapdh6lem2N  39755  mapdh6aN  39756  mapdh6bN  39758  mapdh6cN  39759  mapdh6dN  39760  mapdh6eN  39761  mapdh6fN  39762  mapdh6gN  39763  mapdh6hN  39764  mapdh6iN  39765  mapdh7eN  39769  mapdh7cN  39770  mapdh7dN  39771  mapdh7fN  39772  mapdh75e  39773  mapdh75fN  39776  hvmaplfl  39788  mapdhvmap  39790  mapdh8aa  39797  mapdh8ab  39798  mapdh8ad  39800  mapdh8b  39801  mapdh8c  39802  mapdh8d0N  39803  mapdh8d  39804  mapdh8e  39805  mapdh9a  39810  mapdh9aOLDN  39811  hdmap1val2  39821  hdmap1eq  39822  hdmap1valc  39824  hdmap1eq2  39826  hdmap1eq4N  39827  hdmap1l6lem1  39828  hdmap1l6lem2  39829  hdmap1l6a  39830  hdmap1l6b  39832  hdmap1l6c  39833  hdmap1l6d  39834  hdmap1l6e  39835  hdmap1l6f  39836  hdmap1l6g  39837  hdmap1l6h  39838  hdmap1l6i  39839  hdmap1eulem  39843  hdmap1eulemOLDN  39844  hdmapcl  39851  hdmapval2lem  39852  hdmapval0  39854  hdmapeveclem  39855  hdmapevec  39856  hdmapval3lemN  39858  hdmapval3N  39859  hdmap10lem  39860  hdmap11lem1  39862  hdmap11lem2  39863  hdmapnzcl  39866  hdmaprnlem3N  39871  hdmaprnlem3uN  39872  hdmaprnlem4N  39874  hdmaprnlem7N  39876  hdmaprnlem8N  39877  hdmaprnlem9N  39878  hdmaprnlem3eN  39879  hdmaprnlem16N  39883  hdmap14lem1  39889  hdmap14lem2N  39890  hdmap14lem3  39891  hdmap14lem4a  39892  hdmap14lem6  39894  hdmap14lem8  39896  hdmap14lem9  39897  hdmap14lem10  39898  hdmap14lem11  39899  hdmap14lem12  39900  hgmaprnlem1N  39917  hgmaprnlem2N  39918  hgmaprnlem3N  39919  hgmaprnlem4N  39920  hdmapip1  39937  hdmapinvlem1  39939  hdmapinvlem2  39940  hdmapinvlem3  39941  hdmapinvlem4  39942  hdmapglem5  39943  hgmapvvlem1  39944  hgmapvvlem2  39945  hgmapvvlem3  39946  hdmapglem7a  39948  hdmapglem7b  39949  hdmapglem7  39950  nelsubginvcld  40227  nelsubgcld  40228  nelsubgsubcld  40229  prjspnfv01  40468  prjspner01  40469  prjspner1  40470  dffltz  40478  qirropth  40737  rmxyneg  40749  rmxm1  40763  rmxluc  40765  rmxdbl  40768  ltrmxnn0  40778  jm2.19lem1  40818  jm2.23  40825  rmxdiophlem  40844  aomclem2  40887  inaex  41922  bccm1k  41967  dstregt0  42827  fprodexp  43142  fprodabs2  43143  mccllem  43145  fprodcnlem  43147  climrec  43151  climdivf  43160  islpcn  43187  lptre2pt  43188  0ellimcdiv  43197  reclimc  43201  divlimc  43204  cncficcgt0  43436  dvdivf  43470  stoweidlem34  43582  stoweidlem43  43591  etransclem46  43828  etransclem47  43829  etransclem48  43830  hsphoidmvle2  44130  hsphoidmvle  44131  hoidmvlelem3  44142  hoidmvlelem4  44143  hspdifhsp  44161  readdcnnred  44806  resubcnnred  44807  recnmulnred  44808  cndivrenred  44809  zrzeroorngc  45571  zrtermoringc  45639  zrninitoringc  45640  nzerooringczr  45641