Theorem eldifad 3895

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886

This theorem is referenced by:  xpdifid  6060  unblem1  8996  cantnflem3  9379  cantnflem4  9380  oef1o  9386  infxpenc  9705  acndom2  9741  ackbij1lem18  9924  infpssrlem3  9992  fin23lem26  10012  fin23lem30  10029  pwfseqlem4a  10348  expclz  13735  symgextf  18940  pmtrfinv  18984  symggen  18993  efgsdmi  19253  efgs1b  19257  efgsp1  19258  efgsres  19259  efgredlemf  19262  efgredlemd  19265  efgredlemc  19266  efgredlem  19268  efgrelexlemb  19271  gsum2d2lem  19489  pgpfac1lem2  19593  pgpfac1lem3a  19594  pgpfac1lem3  19595  pgpfac1lem4  19596  isdrng2  19916  lvecinv  20290  lspsncmp  20293  lspsnne1  20294  lspsnnecom  20296  lspabs2  20297  lspsneu  20300  lspdisjb  20303  lspexch  20306  lspindp1  20310  lvecindp2  20316  lspsolv  20320  lspsnat  20322  lsppratlem1  20324  lsppratlem2  20325  fidomndrnglem  20491  frlmssuvc2  20912  maducoeval2  21697  hauscmplem  22465  1stccnp  22521  imasdsf1olem  23434  rrxmetlem  24476  divcncf  24516  dvrec  25024  dvmptdiv  25043  ftc1lem6  25110  elqaalem1  25384  elqaalem3  25386  ulmdvlem3  25466  abelthlem6  25500  abelthlem7a  25501  abelthlem7  25502  logtayl  25720  dmgmn0  26080  dmgmaddnn0  26081  dmgmdivn0  26082  lgamgulmlem2  26084  lgamgulmlem3  26085  lgamgulmlem5  26087  lgamgulmlem6  26088  lgamgulm2  26090  lgambdd  26091  lgamucov  26092  lgamcvg2  26109  gamcvg  26110  gamcvg2lem  26113  ftalem3  26129  lgsqrlem1  26399  lgsqrlem2  26400  lgsqrlem3  26401  lgsqrlem4  26402  lgseisenlem1  26428  lgseisenlem2  26429  lgseisenlem3  26430  lgseisenlem4  26431  lgseisen  26432  lgsquadlem1  26433  lgsquadlem2  26434  lgsquadlem3  26435  chebbnd1lem1  26522  dchrisum0re  26566  dchrisum0lema  26567  dchrisum0lem1b  26568  dchrisum0lem1  26569  dchrisum0lem2a  26570  dchrisum0lem2  26571  tgisline  26892  elntg  27255  uhgrss  27337  upgrex  27365  edguhgr  27402  1loopgrvd0  27774  disjiunel  30836  suppovss  30919  fvdifsupp  30920  gsumhashmul  31218  odpmco  31257  pmtrcnel  31260  pmtrcnelor  31262  cycpmco2f1  31293  cycpmco2rn  31294  cycpmco2lem1  31295  cycpmco2lem2  31296  cycpmco2lem3  31297  cycpmco2lem4  31298  cycpmco2lem5  31299  cycpmco2lem6  31300  cycpmco2lem7  31301  cycpmco2  31302  cyc3co2  31309  tocyccntz  31313  cyc3conja  31326  lindssn  31475  lindfpropd  31478  elrspunidl  31508  lindsunlem  31607  fedgmullem1  31612  fedgmullem2  31613  submatminr1  31662  qtophaus  31688  qqhval2  31832  esummono  31922  gsumesum  31927  esum2dlem  31960  measvuni  32082  fiunelcarsg  32183  sitgclg  32209  sitgaddlemb  32215  eulerpartlemsv2  32225  eulerpartlemsv3  32228  eulerpartlemgc  32229  eulerpartlemv  32231  signstfvneq0  32451  signstfvcl  32452  signstfveq0a  32455  signstfveq0  32456  signsvfn  32461  signsvtp  32462  signsvtn  32463  signsvfpn  32464  signsvfnn  32465  signlem0  32466  hgt750leme  32538  iprodgam  33614  poimirlem2  35706  rrndstprj2  35916  lsatelbN  36947  lsatfixedN  36950  lkreqN  37111  lkrlspeqN  37112  dochnel2  39333  dochnel  39334  djhcvat42  39356  dochsnshp  39394  dochexmidat  39400  dochsnkr  39413  dochsnkr2  39414  dochsnkr2cl  39415  dochflcl  39416  dochfl1  39417  dochfln0  39418  lcfl6lem  39439  lcfl7lem  39440  lcfl8b  39445  lclkrlem2a  39448  lclkrlem2b  39449  lclkrlem2c  39450  lclkrlem2d  39451  lclkrlem2e  39452  lclkrlem2f  39453  lcfrlem14  39497  lcfrlem15  39498  lcfrlem16  39499  lcfrlem17  39500  lcfrlem18  39501  lcfrlem19  39502  lcfrlem20  39503  lcfrlem21  39504  lcfrlem23  39506  lcfrlem25  39508  lcfrlem26  39509  lcfrlem35  39518  lcfrlem36  39519  mapdn0  39610  mapdpglem29  39641  mapdpglem24  39645  baerlem3lem1  39648  baerlem5alem1  39649  baerlem5blem1  39650  baerlem3lem2  39651  baerlem5alem2  39652  baerlem5blem2  39653  baerlem5amN  39657  baerlem5bmN  39658  baerlem5abmN  39659  mapdindp0  39660  mapdindp1  39661  mapdindp2  39662  mapdindp3  39663  mapdindp4  39664  mapdheq2  39670  mapdheq4lem  39672  mapdheq4  39673  mapdh6lem1N  39674  mapdh6lem2N  39675  mapdh6aN  39676  mapdh6bN  39678  mapdh6cN  39679  mapdh6dN  39680  mapdh6eN  39681  mapdh6fN  39682  mapdh6gN  39683  mapdh6hN  39684  mapdh6iN  39685  mapdh7eN  39689  mapdh7cN  39690  mapdh7dN  39691  mapdh7fN  39692  mapdh75e  39693  mapdh75fN  39696  hvmaplfl  39708  mapdhvmap  39710  mapdh8aa  39717  mapdh8ab  39718  mapdh8ad  39720  mapdh8b  39721  mapdh8c  39722  mapdh8d0N  39723  mapdh8d  39724  mapdh8e  39725  mapdh9a  39730  mapdh9aOLDN  39731  hdmap1val2  39741  hdmap1eq  39742  hdmap1valc  39744  hdmap1eq2  39746  hdmap1eq4N  39747  hdmap1l6lem1  39748  hdmap1l6lem2  39749  hdmap1l6a  39750  hdmap1l6b  39752  hdmap1l6c  39753  hdmap1l6d  39754  hdmap1l6e  39755  hdmap1l6f  39756  hdmap1l6g  39757  hdmap1l6h  39758  hdmap1l6i  39759  hdmap1eulem  39763  hdmap1eulemOLDN  39764  hdmapcl  39771  hdmapval2lem  39772  hdmapval0  39774  hdmapeveclem  39775  hdmapevec  39776  hdmapval3lemN  39778  hdmapval3N  39779  hdmap10lem  39780  hdmap11lem1  39782  hdmap11lem2  39783  hdmapnzcl  39786  hdmaprnlem3N  39791  hdmaprnlem3uN  39792  hdmaprnlem4N  39794  hdmaprnlem7N  39796  hdmaprnlem8N  39797  hdmaprnlem9N  39798  hdmaprnlem3eN  39799  hdmaprnlem16N  39803  hdmap14lem1  39809  hdmap14lem2N  39810  hdmap14lem3  39811  hdmap14lem4a  39812  hdmap14lem6  39814  hdmap14lem8  39816  hdmap14lem9  39817  hdmap14lem10  39818  hdmap14lem11  39819  hdmap14lem12  39820  hgmaprnlem1N  39837  hgmaprnlem2N  39838  hgmaprnlem3N  39839  hgmaprnlem4N  39840  hdmapip1  39857  hdmapinvlem1  39859  hdmapinvlem2  39860  hdmapinvlem3  39861  hdmapinvlem4  39862  hdmapglem5  39863  hgmapvvlem1  39864  hgmapvvlem2  39865  hgmapvvlem3  39866  hdmapglem7a  39868  hdmapglem7b  39869  hdmapglem7  39870  nelsubginvcld  40146  nelsubgcld  40147  nelsubgsubcld  40148  prjspnfv01  40382  prjspner01  40383  prjspner1  40384  dffltz  40387  qirropth  40646  rmxyneg  40658  rmxm1  40672  rmxluc  40674  rmxdbl  40677  ltrmxnn0  40687  jm2.19lem1  40727  jm2.23  40734  rmxdiophlem  40753  aomclem2  40796  inaex  41804  bccm1k  41849  dstregt0  42709  fprodexp  43025  fprodabs2  43026  mccllem  43028  fprodcnlem  43030  climrec  43034  climdivf  43043  islpcn  43070  lptre2pt  43071  0ellimcdiv  43080  reclimc  43084  divlimc  43087  cncficcgt0  43319  dvdivf  43353  stoweidlem34  43465  stoweidlem43  43474  etransclem46  43711  etransclem47  43712  etransclem48  43713  hsphoidmvle2  44013  hsphoidmvle  44014  hoidmvlelem3  44025  hoidmvlelem4  44026  hspdifhsp  44044  readdcnnred  44683  resubcnnred  44684  recnmulnred  44685  cndivrenred  44686  zrzeroorngc  45448  zrtermoringc  45516  zrninitoringc  45517  nzerooringczr  45518