Theorem eleqtrrdi 2876

Description: A membership and equality inference. (Contributed by NM, 24-Apr-2005.)

Hypotheses

Ref	Expression
eleqtrrdi.1	⊢ (𝜑 → 𝐴 ∈ 𝐵)
eleqtrrdi.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
eleqtrrdi	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eleqtrrdi

Step	Hyp	Ref	Expression
1		eleqtrrdi.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		eleqtrrdi.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2774	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eleqtrdi 2875	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146

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-ex 1813  df-cleq 2757  df-clel 2840

This theorem is used by:  3eltr4g  2882  srcmpltd  4439  brelrng  5933  elabrex  7245  elabrexg  7246  fliftel1  7317  ovidig  7561  unielxp  8030  tfrlem11  8381  rdglim  8419  seqomlem4  8446  2oconcl  8494  ecopqsi  8774  erov  8818  eroprf  8819  sbthlem2  9083  dffi3  9398  ixpiunwdom  9559  cantnfcl  9643  r1lim  9751  rankwflemb  9772  pwwf  9786  unwf  9789  rankwflem  9794  uniwf  9798  rankpwi  9802  rankr1g  9811  r1pw  9824  r1rankid  9838  rankuni  9842  djulcl  9912  djurcl  9913  inlresf  9916  inrresf  9918  djuun  9928  cardlim  9974  infxpenlem  10013  alephfp  10108  cfsmolem  10269  alephsing  10275  hsmexlem4  10428  axdc3lem2  10450  numth3  10469  iunfo  10540  konigthlem  10570  iunctb  10576  canthwelem  10652  canthwe  10653  r1limwun  10738  inar1  10777  inatsk  10780  gruina  10820  grur1  10822  tskmval  10841  tskmcl  10843  pinq  10929  dmrecnq  10970  addclsr  11085  mulclsr  11086  axaddf  11147  axmulf  11148  peano2nn  12262  uztrn2  12899  eluz2nn  12930  peano2uzs  12944  uzsupss  12982  uzsup  13916  uzrdgfni  14014  uzrdgsuci  14016  fsuppmapnn0fiub  14047  seqf  14079  ser0  14110  bcm1k  14371  bcp1nk  14373  bcpasc  14377  hashprdifel  14454  fz1isolem  14518  pr2pwpr  14536  tpf  14556  ccats1val2  14687  rexuzre  15430  limsupgre  15558  climconst  15620  rlimclim1  15622  climrlim2  15624  clim2ser  15732  clim2ser2  15733  iserex  15734  isermulc2  15735  iserle  15737  isercolllem3  15744  isercoll2  15746  climsup  15747  iseraltlem2  15760  iseraltlem3  15761  zsum  15794  isumclim3  15835  isumadd  15843  fsump1i  15845  iserabs  15892  cvgcmp  15893  cvgcmpub  15894  cvgcmpce  15895  abscvgcvg  15896  isumshft  15918  isumsplit  15919  isum1p  15920  isumrpcl  15922  isumsup2  15925  climcndslem1  15928  cvgrat  15962  clim2prod  15967  clim2div  15968  prodf1  15970  ntrivcvgn0  15977  ntrivcvgtail  15979  fprodntriv  16021  fprodabs  16053  fprodeq0  16054  iprodclim3  16079  iprodmul  16082  ef0lem  16156  fprodefsum  16173  rpnnen2lem3  16296  dvdsflip  16399  fzo0dvdseq  16405  bitsinv1  16524  smupval  16570  smueqlem  16572  seq1st  16653  algr0  16654  prmind2  16767  crth  16861  eulerthlem2  16865  prmdiv  16868  pockthlem  16989  pockthg  16990  unbenlem  16992  prmunb  16998  prmgaplem7  17141  strfv2d  17285  imasvscaval  17616  oppccatid  17799  oppccatf  17808  epii  17824  fthepi  18011  funcestrcsetclem3  18222  funcsetcestrclem3  18236  yon12  18345  yon2  18346  yonedalem4c  18357  yonedalem22  18358  yonedalem3b  18359  yonedainv  18361  acsmapd  18634  chnub  18702  chnccats1  18705  chnccat  18706  mgm2nsgrplem1  19019  mgm2nsgrplem2  19020  mgm2nsgrplem3  19021  sgrp2nmndlem1  19024  sgrp2rid2  19027  ghmqusker  19403  cntrsubgnsg  19459  symgpssefmnd  19512  pmtrrn  19573  gexcl3  19703  efgi  19835  efgi2  19841  efgs1b  19852  efgredlemg  19858  efgredlemd  19860  frgpnabllem1  19989  cycsubgcyg  20017  gsumzaddlem  20037  dprdwd  20129  dprd2da  20160  rhmopp  20658  lsppratlem3  21325  lsppratlem4  21326  lbsextlem2  21335  lidl0ALT  21406  lidl1ALT  21409  2idl0  21451  2idl1  21452  rhmpreimaprmidl  21531  ssdifidllem  21536  ssdifidl  21537  domnchr  21734  znf1o  21753  mplsubrglem  22205  mpfconst  22312  mpfproj  22313  mpfind  22318  mhpmulcl  22364  pf1const  22558  pf1id  22559  mpfpf1  22563  pf1mpf  22564  madetsumid  22670  slesolex  22891  pmatcoe1fsupp  22910  mat2pmatbas0  22936  pmatcollpw  22990  pm2mpf1  23008  isclo  23296  indiscld  23300  restntr  23391  ordtbaslem  23397  ordtbas2  23400  lmconst  23470  lmss  23507  conncompid  23640  2ndcomap  23668  locfincmp  23736  comppfsc  23742  xkouni  23809  txcls  23814  ptclsg  23825  uptx  23835  txindis  23844  tx1stc  23860  cnmpt1res  23886  tgqtop  23922  uffix  24131  cnpflf2  24210  ptcmplem2  24263  ptcmplem4  24265  tgpconncomp  24323  tsmsfbas  24338  fmucnd  24501  prdsxmetlem  24578  imasdsf1olem  24583  prdsbl  24701  blcvx  25008  xrsmopn  25023  xrge0tsms  25045  metdcn2  25050  expcncf  25138  cnmpopc  25140  icchmeo  25153  iccpnfhmeo  25157  cnheibor  25167  evth  25171  evth2  25172  lebnumlem2  25174  lebnumii  25178  reparphti  25209  cfilfcls  25486  minveclem2  25638  minveclem3  25641  minveclem4  25644  ovoliunlem1  25714  ovolicc1  25728  iundisj  25760  volsup  25768  uniioombllem3  25797  vitalilem2  25821  vitalilem3  25822  mbfsup  25876  mbfinf  25877  mbflimsup  25878  itg2monolem1  25962  limcflflem  26092  limccnp  26103  limccnp2  26104  dvidlem  26127  dvn2bss  26142  cpnres  26149  dvcobr  26158  dvrec  26167  c1liplem1  26208  dvcnvrelem2  26230  dvfsumrlimf  26237  dvfsumlem1  26238  dvfsumlem2  26239  dvfsumlem3  26240  dvfsumlem4  26241  dvfsumrlim  26243  dvfsum2  26246  coeeulem  26434  coeid3  26450  plycn  26471  dvntaylp  26587  taylthlem1  26589  taylthlem2  26590  ulm2  26601  ulmshftlem  26605  ulmshft  26606  ulm0  26607  ulmcn  26615  ulmdvlem3  26618  ulmdv  26619  mtest  26620  mtestbdd  26621  dvradcnv  26637  psercn2  26639  psercn  26642  pserdv  26645  abelth  26657  efif1olem2  26761  efif1olem4  26763  efifo  26765  eff1olem  26766  logcn  26865  dvloglem  26866  cxpcn3  26966  resqrtcn  26967  sqrtcn  26968  logbleb  27001  logblt  27002  asinneg  27104  atanlogsub  27134  atanbnd  27144  ressatans  27152  leibpilem2  27159  xrlimcnp  27186  efrlim  27187  scvxcvx  27203  ppiub  27421  chtub  27429  logexprlim  27442  lgseisenlem1  27592  rplogsumlem1  27701  rplogsumlem2  27702  dchrisumlem2  27707  dchrisum0flb  27727  logdivbnd  27773  pntlem3  27826  dfnns2  28618  tgcgr4  28853  ltgov  28919  f1otrg  29277  eengtrkg  29393  iedgedg  29457  ushgredgedgloop  29641  subgruhgredgd  29694  uvtxupgrres  29818  umgr2v2evd2  29937  edginwlk  30044  wlk1walk  30048  crctcshwlkn0lem6  30233  wlkiswwlks1  30285  minvecolem1  31299  minvecolem2  31300  minvecolem4  31305  htthlem  31342  5oalem2  32080  3oalem2  32088  iundisjf  33007  fmptco1f1o  33051  xppreima  33063  xppreima2  33069  dfcnv2  33093  ccatws1f1o  33339  gsumhashmul  33453  xrge0tsmsd  33459  gsumwrd2dccatlem  33463  odpmco  33472  pmtrcnelor  33477  fzo0pmtrlast  33478  wrdpmtrlast  33479  pmtrto1cl  33485  psgnfzto1stlem  33486  fzto1stfv1  33487  fzto1st  33489  fzto1stinvn  33490  psgnfzto1st  33491  tocycf  33503  cycpmco2lem7  33518  cycpmco2  33519  cycpmrn  33529  cyc3evpm  33536  cyc3genpmlem  33537  cycpmgcl  33539  cyc3conja  33543  elrgspnlem1  33628  elrgspnlem2  33629  elrgspnlem3  33630  elrgspnlem4  33631  elrgspnsubrunlem1  33633  nsgmgc  33787  nsgqusf1olem1  33788  nsgqusf1olem2  33789  ssmxidllem  33822  drngmxidlr  33826  opprqus1r  33840  qsdrngilem  33842  qsdrngi  33843  rsprprmprmidlb  33879  rprmirredb  33888  1arithufdlem1  33900  1arithufdlem2  33901  1arithufdlem3  33902  1arithufdlem4  33903  fply1  33914  ply1degltel  33950  ply1degleel  33951  ply1degltlss  33952  mplmulmvr  33995  psrmon  34005  psrmonprod  34008  esplylem  34022  esplyfv1  34025  esplysply  34027  esplyind  34031  ply1degltdimlem  34078  ply1degltdim  34079  algextdeglem4  34176  algextdeglem6  34178  algextdeglem7  34179  algextdeglem8  34180  nn0constr  34217  smatlem  34253  smatcl  34258  zartopn  34331  zarmxt1  34336  tpr2rico  34368  xrmulc1cn  34386  xrge0mulc1cn  34397  esumpfinvallem  34530  ldgenpisyslem1  34620  dynkin  34624  brfae  34705  sxbrsigalem3  34729  dya2icoseg2  34735  omsmeas  34780  sibfof  34797  sseqmw  34848  sseqf  34849  sseqp1  34852  fiblem  34855  fibp1  34858  probfinmeasbALTV  34886  repr0  35065  reprpmtf1o  35080  hgt750lemg  35108  bnj1379  35285  fineqvnttrclselem3  35595  subfacp1lem5  35715  subfacp1lem6  35716  cvxpconn  35773  cvxsconn  35774  cvmliftlem6  35821  cvmliftlem8  35823  cvmliftlem10  35825  cvmlift2lem6  35839  cvmlift2lem11  35844  cvmlift2lem12  35845  2goelgoanfmla1  35955  prv1n  35962  msubff  36061  msubco  36062  elmsta  36079  msubff1  36087  mvhf  36089  msubvrs  36091  iprodefisumlem  36271  filnetlem3  36950  ttcid  37062  ttcwf  37094  knoppcnlem10  37150  knoppcnlem11  37151  icoreunrn  38064  icoreelrn  38066  ralssiun  38112  poimirlem3  38333  poimirlem16  38346  poimirlem17  38347  poimirlem19  38349  poimirlem30  38360  dvasin  38414  cover2  38426  upixp  38440  sdclem1  38454  fdc  38456  caushft  38472  ismtyres  38519  rrncmslem  38543  isfld2  38716  presuc  39207  osumcllem10N  40799  pexmidlem7N  40810  dihglblem2N  42128  lcfrvalsnN  42375  lcfrlem5  42380  lcfrlem6  42381  lcfrlem27  42403  lcfrlem37  42413  aks6d1c1p4  42938  aks6d1c1p7  42940  aks6d1c1p8  42942  evl1gprodd  42944  aks6d1c2lem4  42954  aks6d1c5lem3  42964  aks6d1c6lem2  42998  prjspvs  43402  0prjspnrel  43419  monotuz  43728  expdiophlem1  43808  kelac2  43852  naddwordnexlem4  44188  grurankcld  45017  dvgrat  45082  nzss  45087  uzmptshftfval  45116  binomcxplemnotnn0  45126  orbitinit  45725  orbitcl  45726  permaxinf2lem  45781  refsumcn  45810  rfcnpre2  45811  rfcnpre3  45813  rfcnpre4  45814  disjf1o  45969  unirnmap  45984  unirnmapsn  45990  ssmapsn  45992  mptssid  46016  allbutfi  46168  eluzd  46183  uzidd2  46190  ressiocsup  46330  ressioosup  46331  ressiooinf  46333  fsumsermpt  46355  climexp  46381  climinf  46382  climsuse  46384  sumnnodd  46406  limsupresico  46474  limsupubuzlem  46486  limsupresxr  46540  liminfresxr  46541  liminfresico  46545  limsup10exlem  46546  cnrefiisplem  46603  cncfiooicclem1  46667  dvsinax  46687  itgsinexplem1  46728  fvvolioof  46763  fvvolicof  46765  stoweidlem14  46788  stoweidlem16  46790  stoweidlem31  46805  stoweidlem34  46808  stoweidlem36  46810  stoweidlem43  46817  stoweidlem46  46820  stoweidlem47  46821  stoweidlem52  46826  stoweidlem55  46829  stoweidlem57  46831  dirkercncf  46881  fourierdlem20  46901  fourierdlem42  46923  fourierdlem51  46931  fourierdlem54  46934  fourierdlem62  46942  fourierdlem71  46951  fourierdlem80  46960  fourierdlem114  46994  fouriersw  47005  ioorrnopnlem  47078  ioorrnopnxrlem  47080  salexct3  47116  salgencntex  47117  salgensscntex  47118  subsalsal  47133  sge0fodjrnlem  47190  sge0isum  47201  sge0seq  47220  sge0reuz  47221  sge0reuzb  47222  meadjiunlem  47239  meaiininclem  47260  carageniuncllem1  47295  caratheodorylem1  47300  hoiprodp1  47362  hoidmv1lelem1  47365  hoidmv1lelem2  47366  hoidmv1le  47368  hoidmvlelem1  47369  hoidmvlelem2  47370  hoidmvlelem3  47371  voncmpl  47395  hoiqssbl  47399  smflimlem2  47546  smfsuplem1  47585  smfsuplem3  47587  fsupdm  47616  finfdm  47620  cfsetsnfsetf  47855  fcores  47864  afvres  47969  afv2res  48036  fundcmpsurinjimaid  48220  iccpartigtl  48232  sprsymrelf  48304  prproropf1olem2  48313  uhgrimedgi  48715  isuspgrim0lem  48718  isuspgrimlem  48720  ushggricedg  48752  grimedg  48760  usgrgrtrirex  48775  isubgr3stgrlem7  48797  uspgrlimlem4  48816  grlimprclnbgr  48821  gpgiedgdmellem  48871  gpg3kgrtriex  48914  funcringcsetcALTV2lem3  49116  funcringcsetclem3ALTV  49139  lindslinindsimp2lem5  49301  rrxsphere  49587  line2  49591  iooii  49755  icccldii  49756  iscnrm3rlem3  49779  eloppf2  49971  oppcup  50044  natoppf  50066  zeroo2  50071  oppfdiag1  50251  oppfdiag  50253  2arwcat  50437  incat  50438  lmddu  50504  onsetreclem3  50544  amgmwlem  50709