Theorem eldifad 3918

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∈ wcel 2146   ∖ cdif 3903

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-dif 3909

This theorem is used by:  xpdifid  6167  xpdifcnvepel  6168  fvdifsupp  8173  unblem1  9259  cantnflem3  9667  cantnflem4  9668  oef1o  9674  infxpenc  10018  acndom2  10054  ackbij1lem18  10235  infpssrlem3  10304  fin23lem26  10324  fin23lem30  10341  pwfseqlem4a  10663  elfzodif0  13818  expclz  14140  pfxchn  18690  chnind  18701  chnccats1  18705  chnccat  18706  symgextf  19533  pmtrfinv  19577  symggen  19586  efgsdmi  19848  efgs1b  19852  efgsp1  19853  efgsres  19854  efgredlemf  19857  efgredlemd  19860  efgredlemc  19861  efgredlem  19863  efgrelexlemb  19866  gsum2d2lem  20089  pgpfac1lem2  20193  pgpfac1lem3a  20194  pgpfac1lem3  20195  pgpfac1lem4  20196  zrzeroorngc  20795  zrtermoringc  20826  zrninitoringc  20827  domneq0r  20874  isdrng4  20891  isdrng2  20895  fidomndrnglem  20928  lvecinv  21289  lspsncmp  21292  lspsnne1  21293  lspsnnecom  21295  lspabs2  21296  lspsneu  21299  lspdisjb  21302  lspexch  21305  lspindp1  21309  lvecindp2  21315  lspsolv  21319  lspsnat  21321  lsppratlem1  21323  lsppratlem2  21324  drngidl  21437  prmidlsubm  21539  nzerooringczr  21682  frlmssuvc2  21997  evls1fpws  22581  maducoeval2  22849  hauscmplem  23615  1stccnp  23672  imasdsf1olem  24583  rrxmetlem  25619  divcncf  25659  dvrec  26167  dvmptdiv  26186  ftc1lem6  26253  elqaalem1  26533  elqaalem3  26535  ulmdvlem3  26618  abelthlem6  26652  abelthlem7a  26653  abelthlem7  26654  logtayl  26878  dmgmn0  27243  dmgmaddnn0  27244  dmgmdivn0  27245  lgamgulmlem2  27247  lgamgulmlem3  27248  lgamgulmlem5  27250  lgamgulmlem6  27251  lgamgulm2  27253  lgambdd  27254  lgamucov  27255  lgamcvg2  27272  gamcvg  27273  gamcvg2lem  27276  ftalem3  27292  lgsqrlem1  27563  lgsqrlem2  27564  lgsqrlem3  27565  lgsqrlem4  27566  lgseisenlem1  27592  lgseisenlem2  27593  lgseisenlem3  27594  lgseisenlem4  27595  lgseisen  27596  lgsquadlem1  27597  lgsquadlem2  27598  lgsquadlem3  27599  chebbnd1lem1  27686  dchrisum0re  27730  dchrisum0lema  27731  dchrisum0lem1b  27732  dchrisum0lem1  27733  dchrisum0lem2a  27734  dchrisum0lem2  27735  tgisline  28953  oppmir  29089  tgelrnpln  29111  elplng  29115  elplngid  29117  plngcplem  29120  plngrotlem1  29122  plngrotlem2  29123  plngrotlem3  29124  plngrot  29125  lnssplnglem  29126  lnssplng  29127  plngmiropp  29129  nhpmirhp  29133  ragsupplcgra  29201  perpeqlem  29203  dfprlng2  29254  perpprlng  29257  prlngex  29258  prlngmolem1  29259  prlngmolem2  29260  prlngeu  29262  prlngmid2  29268  elntg  29391  uhgrss  29471  upgrex  29499  edguhgr  29536  1loopgrvd0  29914  disjiunel  33014  suppovss  33099  nn0difffzod  33221  gsumfs2d  33447  gsumhashmul  33453  suppgsumssiun  33458  odpmco  33472  pmtrcnel  33475  pmtrcnelor  33477  cycpmco2f1  33510  cycpmco2rn  33511  cycpmco2lem1  33512  cycpmco2lem2  33513  cycpmco2lem3  33514  cycpmco2lem4  33515  cycpmco2lem5  33516  cycpmco2lem6  33517  cycpmco2lem7  33518  cycpmco2  33519  cyc3co2  33526  tocyccntz  33530  cyc3conja  33543  fxpsdrg  33561  elrgspnlem2  33629  elrgspnlem4  33631  elrgspnsubrunlem2  33634  domnprodn0  33664  domnprodeq0  33665  fracfld  33695  lindssn  33757  lindfpropd  33761  elrspunidl  33802  elrspunsn  33803  mxidlmaxv  33817  mxidlirredi  33820  opprqusdrng  33841  qsdrnglem2  33844  dflringlem  33850  dflringlem2  33851  rprmcl  33874  rprmirred  33887  pidufd  33899  1arithufdlem3  33902  dfufd2  33906  zringfrac  33910  deg1prod  33939  ply1dg3rt0irred  33940  gsummoncoe1fzo  33953  mplvrpmrhm  34003  psrgsum  34004  psrmonprod  34008  esplyfval2  34021  lindsunlem  34080  fedgmullem1  34085  fedgmullem2  34086  assafld  34093  fldextrspunlsp  34130  extdgfialglem2  34149  irngnminplynz  34168  constrextdg2lem  34204  constrfiss  34207  constrsdrg  34231  submatminr1  34266  qtophaus  34292  qqhval2  34438  esummono  34510  gsumesum  34515  esum2dlem  34548  measvuni  34671  fiunelcarsg  34773  sitgclg  34799  sitgaddlemb  34805  eulerpartlemsv2  34815  eulerpartlemsv3  34818  eulerpartlemgc  34819  eulerpartlemv  34821  signstfvneq0  35026  signstfvcl  35027  signstfveq0a  35030  signstfveq0  35031  signsvfn  35036  signsvtp  35037  signsvtn  35038  signsvfpn  35039  signsvfnn  35040  signlem0  35041  hgt750leme  35112  onvf1odlem4  35649  iprodgam  36273  ttcwf2  37095  mh-inf3f1  37111  poimirlem2  38332  rrndstprj2  38542  lsatelbN  39840  lsatfixedN  39843  lkreqN  40004  lkrlspeqN  40005  dochnel2  42226  dochnel  42227  djhcvat42  42249  dochsnshp  42287  dochexmidat  42293  dochsnkr  42306  dochsnkr2  42307  dochsnkr2cl  42308  dochflcl  42309  dochfl1  42310  dochfln0  42311  lcfl6lem  42332  lcfl7lem  42333  lcfl8b  42338  lclkrlem2a  42341  lclkrlem2b  42342  lclkrlem2c  42343  lclkrlem2d  42344  lclkrlem2e  42345  lclkrlem2f  42346  lcfrlem14  42390  lcfrlem15  42391  lcfrlem16  42392  lcfrlem17  42393  lcfrlem18  42394  lcfrlem19  42395  lcfrlem20  42396  lcfrlem21  42397  lcfrlem23  42399  lcfrlem25  42401  lcfrlem26  42402  lcfrlem35  42411  lcfrlem36  42412  mapdn0  42503  mapdpglem29  42534  mapdpglem24  42538  baerlem3lem1  42541  baerlem5alem1  42542  baerlem5blem1  42543  baerlem3lem2  42544  baerlem5alem2  42545  baerlem5blem2  42546  baerlem5amN  42550  baerlem5bmN  42551  baerlem5abmN  42552  mapdindp0  42553  mapdindp1  42554  mapdindp2  42555  mapdindp3  42556  mapdindp4  42557  mapdheq2  42563  mapdheq4lem  42565  mapdheq4  42566  mapdh6lem1N  42567  mapdh6lem2N  42568  mapdh6aN  42569  mapdh6bN  42571  mapdh6cN  42572  mapdh6dN  42573  mapdh6eN  42574  mapdh6fN  42575  mapdh6gN  42576  mapdh6hN  42577  mapdh6iN  42578  mapdh7eN  42582  mapdh7cN  42583  mapdh7dN  42584  mapdh7fN  42585  mapdh75e  42586  mapdh75fN  42589  hvmaplfl  42601  mapdhvmap  42603  mapdh8aa  42610  mapdh8ab  42611  mapdh8ad  42613  mapdh8b  42614  mapdh8c  42615  mapdh8d0N  42616  mapdh8d  42617  mapdh8e  42618  mapdh9a  42623  mapdh9aOLDN  42624  hdmap1val2  42634  hdmap1eq  42635  hdmap1valc  42637  hdmap1eq2  42639  hdmap1eq4N  42640  hdmap1l6lem1  42641  hdmap1l6lem2  42642  hdmap1l6a  42643  hdmap1l6b  42645  hdmap1l6c  42646  hdmap1l6d  42647  hdmap1l6e  42648  hdmap1l6f  42649  hdmap1l6g  42650  hdmap1l6h  42651  hdmap1l6i  42652  hdmap1eulem  42656  hdmap1eulemOLDN  42657  hdmapcl  42664  hdmapval2lem  42665  hdmapval0  42667  hdmapeveclem  42668  hdmapevec  42669  hdmapval3lemN  42671  hdmapval3N  42672  hdmap10lem  42673  hdmap11lem1  42675  hdmap11lem2  42676  hdmapnzcl  42679  hdmaprnlem3N  42684  hdmaprnlem3uN  42685  hdmaprnlem4N  42687  hdmaprnlem7N  42689  hdmaprnlem8N  42690  hdmaprnlem9N  42691  hdmaprnlem3eN  42692  hdmaprnlem16N  42696  hdmap14lem1  42702  hdmap14lem2N  42703  hdmap14lem3  42704  hdmap14lem4a  42705  hdmap14lem6  42707  hdmap14lem8  42709  hdmap14lem9  42710  hdmap14lem10  42711  hdmap14lem11  42712  hdmap14lem12  42713  hgmaprnlem1N  42730  hgmaprnlem2N  42731  hgmaprnlem3N  42732  hgmaprnlem4N  42733  hdmapip1  42750  hdmapinvlem1  42752  hdmapinvlem2  42753  hdmapinvlem3  42754  hdmapinvlem4  42755  hdmapglem5  42756  hgmapvvlem1  42757  hgmapvvlem2  42758  hgmapvvlem3  42759  hdmapglem7a  42761  hdmapglem7b  42762  hdmapglem7  42763  evl1gprodd  42944  nelsubginvcld  43330  nelsubgcld  43331  nelsubgsubcld  43332  domnexpgn0cl  43351  fidomncyc  43363  prjspnfv01  43416  prjspner01  43417  prjspner1  43418  dffltz  43426  qirropth  43695  rmxyneg  43707  rmxm1  43721  rmxluc  43723  rmxdbl  43726  ltrmxnn0  43736  jm2.19lem1  43776  jm2.23  43783  rmxdiophlem  43802  aomclem2  43842  cantnftermord  44107  inaex  45067  bccm1k  45112  dstregt0  46061  fprodexp  46370  fprodabs2  46371  mccllem  46373  fprodcnlem  46375  climrec  46379  climdivf  46388  islpcn  46413  lptre2pt  46414  0ellimcdiv  46423  reclimc  46427  divlimc  46430  cncficcgt0  46662  dvdivf  46696  stoweidlem34  46808  stoweidlem43  46817  etransclem46  47054  etransclem47  47055  etransclem48  47056  hsphoidmvle2  47359  hsphoidmvle  47360  hoidmvlelem3  47371  hoidmvlelem4  47372  hspdifhsp  47390  readdcnnred  48100  resubcnnred  48101  recnmulnred  48102  cndivrenred  48103