Theorem eldifad 3901

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

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

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-dif 3892

This theorem is referenced by:  xpdifid  6132  fvdifsupp  8121  unblem1  9202  cantnflem3  9612  cantnflem4  9613  oef1o  9619  infxpenc  9940  acndom2  9976  ackbij1lem18  10158  infpssrlem3  10227  fin23lem26  10247  fin23lem30  10264  pwfseqlem4a  10584  elfzodif0  13725  expclz  14046  pfxchn  18576  chnind  18587  chnccats1  18591  chnccat  18592  symgextf  19392  pmtrfinv  19436  symggen  19445  efgsdmi  19707  efgs1b  19711  efgsp1  19712  efgsres  19713  efgredlemf  19716  efgredlemd  19719  efgredlemc  19720  efgredlem  19722  efgrelexlemb  19725  gsum2d2lem  19948  pgpfac1lem2  20052  pgpfac1lem3a  20053  pgpfac1lem3  20054  pgpfac1lem4  20055  zrzeroorngc  20621  zrtermoringc  20652  zrninitoringc  20653  domneq0r  20701  isdrng2  20720  fidomndrnglem  20749  lvecinv  21111  lspsncmp  21114  lspsnne1  21115  lspsnnecom  21117  lspabs2  21118  lspsneu  21121  lspdisjb  21124  lspexch  21127  lspindp1  21131  lvecindp2  21137  lspsolv  21141  lspsnat  21143  lsppratlem1  21145  lsppratlem2  21146  nzerooringczr  21460  frlmssuvc2  21775  evls1fpws  22334  maducoeval2  22605  hauscmplem  23371  1stccnp  23427  imasdsf1olem  24338  rrxmetlem  25374  divcncf  25414  dvrec  25922  dvmptdiv  25941  ftc1lem6  26008  elqaalem1  26285  elqaalem3  26287  ulmdvlem3  26367  abelthlem6  26401  abelthlem7a  26402  abelthlem7  26403  logtayl  26624  dmgmn0  26989  dmgmaddnn0  26990  dmgmdivn0  26991  lgamgulmlem2  26993  lgamgulmlem3  26994  lgamgulmlem5  26996  lgamgulmlem6  26997  lgamgulm2  26999  lgambdd  27000  lgamucov  27001  lgamcvg2  27018  gamcvg  27019  gamcvg2lem  27022  ftalem3  27038  lgsqrlem1  27309  lgsqrlem2  27310  lgsqrlem3  27311  lgsqrlem4  27312  lgseisenlem1  27338  lgseisenlem2  27339  lgseisenlem3  27340  lgseisenlem4  27341  lgseisen  27342  lgsquadlem1  27343  lgsquadlem2  27344  lgsquadlem3  27345  chebbnd1lem1  27432  dchrisum0re  27476  dchrisum0lema  27477  dchrisum0lem1b  27478  dchrisum0lem1  27479  dchrisum0lem2a  27480  dchrisum0lem2  27481  tgisline  28695  elntg  29053  uhgrss  29133  upgrex  29161  edguhgr  29198  1loopgrvd0  29573  disjiunel  32666  suppovss  32754  nn0difffzod  32877  gsumfs2d  33122  gsumhashmul  33128  suppgsumssiun  33133  odpmco  33147  pmtrcnel  33150  pmtrcnelor  33152  cycpmco2f1  33185  cycpmco2rn  33186  cycpmco2lem1  33187  cycpmco2lem2  33188  cycpmco2lem3  33189  cycpmco2lem4  33190  cycpmco2lem5  33191  cycpmco2lem6  33192  cycpmco2lem7  33193  cycpmco2  33194  cyc3co2  33201  tocyccntz  33205  cyc3conja  33218  fxpsdrg  33236  elrgspnlem2  33304  elrgspnlem4  33306  elrgspnsubrunlem2  33309  domnprodn0  33336  domnprodeq0  33337  idomrcanOLD  33343  isdrng4  33356  fracfld  33369  lindssn  33438  lindfpropd  33442  elrspunidl  33488  elrspunsn  33489  drngidl  33493  mxidlmaxv  33528  mxidlirredi  33531  opprqusdrng  33553  qsdrnglem2  33556  rprmcl  33578  rprmirred  33591  pidufd  33603  1arithufdlem3  33606  dfufd2  33610  zringfrac  33614  deg1prod  33643  ply1dg3rt0irred  33644  gsummoncoe1fzo  33657  mplvrpmrhm  33691  psrgsum  33692  psrmonprod  33696  esplyfval2  33709  lindsunlem  33768  fedgmullem1  33773  fedgmullem2  33774  assafld  33781  fldextrspunlsp  33818  extdgfialglem2  33837  irngnminplynz  33856  constrextdg2lem  33892  constrfiss  33895  constrsdrg  33919  submatminr1  33954  qtophaus  33980  qqhval2  34126  esummono  34198  gsumesum  34203  esum2dlem  34236  measvuni  34358  fiunelcarsg  34460  sitgclg  34486  sitgaddlemb  34492  eulerpartlemsv2  34502  eulerpartlemsv3  34505  eulerpartlemgc  34506  eulerpartlemv  34508  signstfvneq0  34716  signstfvcl  34717  signstfveq0a  34720  signstfveq0  34721  signsvfn  34726  signsvtp  34727  signsvtn  34728  signsvfpn  34729  signsvfnn  34730  signlem0  34731  hgt750leme  34802  onvf1odlem4  35288  iprodgam  35924  ttcwf2  36707  mh-inf3f1  36723  poimirlem2  37943  rrndstprj2  38152  lsatelbN  39452  lsatfixedN  39455  lkreqN  39616  lkrlspeqN  39617  dochnel2  41838  dochnel  41839  djhcvat42  41861  dochsnshp  41899  dochexmidat  41905  dochsnkr  41918  dochsnkr2  41919  dochsnkr2cl  41920  dochflcl  41921  dochfl1  41922  dochfln0  41923  lcfl6lem  41944  lcfl7lem  41945  lcfl8b  41950  lclkrlem2a  41953  lclkrlem2b  41954  lclkrlem2c  41955  lclkrlem2d  41956  lclkrlem2e  41957  lclkrlem2f  41958  lcfrlem14  42002  lcfrlem15  42003  lcfrlem16  42004  lcfrlem17  42005  lcfrlem18  42006  lcfrlem19  42007  lcfrlem20  42008  lcfrlem21  42009  lcfrlem23  42011  lcfrlem25  42013  lcfrlem26  42014  lcfrlem35  42023  lcfrlem36  42024  mapdn0  42115  mapdpglem29  42146  mapdpglem24  42150  baerlem3lem1  42153  baerlem5alem1  42154  baerlem5blem1  42155  baerlem3lem2  42156  baerlem5alem2  42157  baerlem5blem2  42158  baerlem5amN  42162  baerlem5bmN  42163  baerlem5abmN  42164  mapdindp0  42165  mapdindp1  42166  mapdindp2  42167  mapdindp3  42168  mapdindp4  42169  mapdheq2  42175  mapdheq4lem  42177  mapdheq4  42178  mapdh6lem1N  42179  mapdh6lem2N  42180  mapdh6aN  42181  mapdh6bN  42183  mapdh6cN  42184  mapdh6dN  42185  mapdh6eN  42186  mapdh6fN  42187  mapdh6gN  42188  mapdh6hN  42189  mapdh6iN  42190  mapdh7eN  42194  mapdh7cN  42195  mapdh7dN  42196  mapdh7fN  42197  mapdh75e  42198  mapdh75fN  42201  hvmaplfl  42213  mapdhvmap  42215  mapdh8aa  42222  mapdh8ab  42223  mapdh8ad  42225  mapdh8b  42226  mapdh8c  42227  mapdh8d0N  42228  mapdh8d  42229  mapdh8e  42230  mapdh9a  42235  mapdh9aOLDN  42236  hdmap1val2  42246  hdmap1eq  42247  hdmap1valc  42249  hdmap1eq2  42251  hdmap1eq4N  42252  hdmap1l6lem1  42253  hdmap1l6lem2  42254  hdmap1l6a  42255  hdmap1l6b  42257  hdmap1l6c  42258  hdmap1l6d  42259  hdmap1l6e  42260  hdmap1l6f  42261  hdmap1l6g  42262  hdmap1l6h  42263  hdmap1l6i  42264  hdmap1eulem  42268  hdmap1eulemOLDN  42269  hdmapcl  42276  hdmapval2lem  42277  hdmapval0  42279  hdmapeveclem  42280  hdmapevec  42281  hdmapval3lemN  42283  hdmapval3N  42284  hdmap10lem  42285  hdmap11lem1  42287  hdmap11lem2  42288  hdmapnzcl  42291  hdmaprnlem3N  42296  hdmaprnlem3uN  42297  hdmaprnlem4N  42299  hdmaprnlem7N  42301  hdmaprnlem8N  42302  hdmaprnlem9N  42303  hdmaprnlem3eN  42304  hdmaprnlem16N  42308  hdmap14lem1  42314  hdmap14lem2N  42315  hdmap14lem3  42316  hdmap14lem4a  42317  hdmap14lem6  42319  hdmap14lem8  42321  hdmap14lem9  42322  hdmap14lem10  42323  hdmap14lem11  42324  hdmap14lem12  42325  hgmaprnlem1N  42342  hgmaprnlem2N  42343  hgmaprnlem3N  42344  hgmaprnlem4N  42345  hdmapip1  42362  hdmapinvlem1  42364  hdmapinvlem2  42365  hdmapinvlem3  42366  hdmapinvlem4  42367  hdmapglem5  42368  hgmapvvlem1  42369  hgmapvvlem2  42370  hgmapvvlem3  42371  hdmapglem7a  42373  hdmapglem7b  42374  hdmapglem7  42375  evl1gprodd  42556  nelsubginvcld  42941  nelsubgcld  42942  nelsubgsubcld  42943  domnexpgn0cl  42968  fidomncyc  42980  prjspnfv01  43057  prjspner01  43058  prjspner1  43059  dffltz  43067  qirropth  43336  rmxyneg  43348  rmxm1  43362  rmxluc  43364  rmxdbl  43367  ltrmxnn0  43377  jm2.19lem1  43417  jm2.23  43424  rmxdiophlem  43443  aomclem2  43483  cantnftermord  43748  inaex  44724  bccm1k  44769  dstregt0  45715  fprodexp  46024  fprodabs2  46025  mccllem  46027  fprodcnlem  46029  climrec  46033  climdivf  46042  islpcn  46067  lptre2pt  46068  0ellimcdiv  46077  reclimc  46081  divlimc  46084  cncficcgt0  46316  dvdivf  46350  stoweidlem34  46462  stoweidlem43  46471  etransclem46  46708  etransclem47  46709  etransclem48  46710  hsphoidmvle2  47013  hsphoidmvle  47014  hoidmvlelem3  47025  hoidmvlelem4  47026  hspdifhsp  47044  readdcnnred  47751  resubcnnred  47752  recnmulnred  47753  cndivrenred  47754