Theorem eleqtrrdi 2880

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 2778	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eleqtrdi 2879	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844

This theorem is referenced by:  3eltr4g  2886  brelrng  5932  elabrex  7241  elabrexg  7242  fliftel1  7309  ovidig  7553  unielxp  8024  tfrlem11  8375  rdglim  8413  seqomlem4  8440  2oconcl  8488  ecopqsi  8768  erov  8812  eroprf  8813  sbthlem2  9076  dffi3  9391  ixpiunwdom  9552  cantnfcl  9636  r1lim  9744  rankwflemb  9765  pwwf  9779  unwf  9782  rankwflem  9787  uniwf  9791  rankpwi  9795  rankr1g  9804  r1pw  9817  r1rankid  9831  rankuni  9835  djulcl  9896  djurcl  9897  inlresf  9900  inrresf  9902  djuun  9912  cardlim  9958  infxpenlem  9997  alephfp  10092  cfsmolem  10254  alephsing  10260  hsmexlem4  10413  axdc3lem2  10435  numth3  10454  iunfo  10523  konigthlem  10553  iunctb  10559  canthwelem  10635  canthwe  10636  r1limwun  10721  inar1  10760  inatsk  10763  gruina  10803  grur1  10805  tskmval  10824  tskmcl  10826  pinq  10912  dmrecnq  10953  addclsr  11068  mulclsr  11069  axaddf  11130  axmulf  11131  peano2nn  12245  uztrn2  12881  eluz2nn  12912  peano2uzs  12926  uzsupss  12964  uzsup  13896  uzrdgfni  13994  uzrdgsuci  13996  fsuppmapnn0fiub  14027  seqf  14059  ser0  14090  bcm1k  14351  bcp1nk  14353  bcpasc  14357  hashprdifel  14434  fz1isolem  14498  pr2pwpr  14516  tpf  14536  ccats1val2  14665  rexuzre  15404  limsupgre  15532  climconst  15594  rlimclim1  15596  climrlim2  15598  clim2ser  15706  clim2ser2  15707  iserex  15708  isermulc2  15709  iserle  15711  isercolllem3  15718  isercoll2  15720  climsup  15721  iseraltlem2  15734  iseraltlem3  15735  zsum  15769  isumclim3  15810  isumadd  15818  fsump1i  15820  iserabs  15867  cvgcmp  15868  cvgcmpub  15869  cvgcmpce  15870  abscvgcvg  15871  isumshft  15893  isumsplit  15894  isum1p  15895  isumrpcl  15897  isumsup2  15900  climcndslem1  15903  cvgrat  15937  clim2prod  15942  clim2div  15943  prodf1  15945  ntrivcvgn0  15952  ntrivcvgtail  15954  fprodntriv  15996  fprodabs  16028  fprodeq0  16029  iprodclim3  16054  iprodmul  16057  ef0lem  16132  fprodefsum  16149  rpnnen2lem3  16272  dvdsflip  16375  fzo0dvdseq  16381  bitsinv1  16500  smupval  16546  smueqlem  16548  seq1st  16629  algr0  16630  prmind2  16743  crth  16837  eulerthlem2  16841  prmdiv  16844  pockthlem  16965  pockthg  16966  unbenlem  16968  prmunb  16974  prmgaplem7  17117  strfv2d  17261  imasvscaval  17592  oppccatid  17775  oppccatf  17784  epii  17800  fthepi  17987  funcestrcsetclem3  18198  funcsetcestrclem3  18212  yon12  18321  yon2  18322  yonedalem4c  18333  yonedalem22  18334  yonedalem3b  18335  yonedainv  18337  acsmapd  18610  chnub  18678  chnccats1  18681  chnccat  18682  mgm2nsgrplem1  18980  mgm2nsgrplem2  18981  mgm2nsgrplem3  18982  sgrp2nmndlem1  18985  sgrp2rid2  18988  ghmqusker  19357  cntrsubgnsg  19413  symgpssefmnd  19466  pmtrrn  19527  gexcl3  19657  efgi  19789  efgi2  19795  efgs1b  19806  efgredlemg  19812  efgredlemd  19814  frgpnabllem1  19943  cycsubgcyg  19971  gsumzaddlem  19991  dprdwd  20083  dprd2da  20114  rhmopp  20592  lsppratlem3  21251  lsppratlem4  21252  lbsextlem2  21261  lidl0ALT  21332  lidl1ALT  21335  2idl0  21370  2idl1  21371  rhmpreimaprmidl  21448  ssdifidllem  21453  ssdifidl  21454  domnchr  21651  znf1o  21670  mplsubrglem  22122  mpfconst  22229  mpfproj  22230  mpfind  22235  mhpmulcl  22281  pf1const  22475  pf1id  22476  mpfpf1  22480  pf1mpf  22481  madetsumid  22587  slesolex  22808  pmatcoe1fsupp  22827  mat2pmatbas0  22853  pmatcollpw  22907  pm2mpf1  22925  isclo  23213  indiscld  23217  restntr  23308  ordtbaslem  23314  ordtbas2  23317  lmconst  23387  lmss  23424  conncompid  23557  2ndcomap  23584  locfincmp  23652  comppfsc  23658  xkouni  23725  txcls  23730  ptclsg  23741  uptx  23751  txindis  23760  tx1stc  23776  cnmpt1res  23802  tgqtop  23838  uffix  24047  cnpflf2  24126  ptcmplem2  24179  ptcmplem4  24181  tgpconncomp  24239  tsmsfbas  24254  fmucnd  24417  prdsxmetlem  24494  imasdsf1olem  24499  prdsbl  24617  blcvx  24924  xrsmopn  24939  xrge0tsms  24961  metdcn2  24966  expcncf  25054  cnmpopc  25056  icchmeo  25069  iccpnfhmeo  25073  cnheibor  25083  evth  25087  evth2  25088  lebnumlem2  25090  lebnumii  25094  reparphti  25125  cfilfcls  25402  minveclem2  25554  minveclem3  25557  minveclem4  25560  ovoliunlem1  25630  ovolicc1  25644  iundisj  25676  volsup  25684  uniioombllem3  25713  vitalilem2  25737  vitalilem3  25738  mbfsup  25792  mbfinf  25793  mbflimsup  25794  itg2monolem1  25878  limcflflem  26008  limccnp  26019  limccnp2  26020  dvidlem  26043  dvn2bss  26058  cpnres  26065  dvcobr  26074  dvrec  26083  c1liplem1  26124  dvcnvrelem2  26146  dvfsumrlimf  26153  dvfsumlem1  26154  dvfsumlem2  26155  dvfsumlem3  26156  dvfsumlem4  26157  dvfsumrlim  26159  dvfsum2  26162  coeeulem  26350  coeid3  26366  plycn  26387  dvntaylp  26500  taylthlem1  26502  taylthlem2  26503  ulm2  26514  ulmshftlem  26518  ulmshft  26519  ulm0  26520  ulmcn  26528  ulmdvlem3  26531  ulmdv  26532  mtest  26533  mtestbdd  26534  dvradcnv  26550  psercn2  26552  psercn  26555  pserdv  26558  abelth  26570  efif1olem2  26674  efif1olem4  26676  efifo  26678  eff1olem  26679  logcn  26778  dvloglem  26779  cxpcn3  26879  resqrtcn  26880  sqrtcn  26881  logbleb  26914  logblt  26915  asinneg  27017  atanlogsub  27047  atanbnd  27057  ressatans  27065  leibpilem2  27072  xrlimcnp  27099  efrlim  27100  scvxcvx  27116  ppiub  27334  chtub  27342  logexprlim  27355  lgseisenlem1  27505  rplogsumlem1  27614  rplogsumlem2  27615  dchrisumlem2  27620  dchrisum0flb  27640  logdivbnd  27686  pntlem3  27739  dfnns2  28531  tgcgr4  28766  ltgov  28832  f1otrg  29161  eengtrkg  29277  iedgedg  29341  ushgredgedgloop  29522  subgruhgredgd  29575  uvtxupgrres  29699  umgr2v2evd2  29818  edginwlk  29925  wlk1walk  29929  crctcshwlkn0lem6  30105  wlkiswwlks1  30157  minvecolem1  31167  minvecolem2  31168  minvecolem4  31173  htthlem  31210  5oalem2  31948  3oalem2  31956  iundisjf  32875  fmptco1f1o  32919  xppreima  32931  xppreima2  32937  dfcnv2  32961  ccatws1f1o  33212  gsumhashmul  33328  xrge0tsmsd  33334  gsumwrd2dccatlem  33338  odpmco  33347  pmtrcnelor  33352  fzo0pmtrlast  33353  wrdpmtrlast  33354  pmtrto1cl  33360  psgnfzto1stlem  33361  fzto1stfv1  33362  fzto1st  33364  fzto1stinvn  33365  psgnfzto1st  33366  tocycf  33378  cycpmco2lem7  33393  cycpmco2  33394  cycpmrn  33404  cyc3evpm  33411  cyc3genpmlem  33412  cycpmgcl  33414  cyc3conja  33418  elrgspnlem1  33503  elrgspnlem2  33504  elrgspnlem3  33505  elrgspnlem4  33506  elrgspnsubrunlem1  33508  nsgmgc  33665  nsgqusf1olem1  33666  nsgqusf1olem2  33667  ssmxidllem  33701  drngmxidlr  33705  opprqus1r  33719  qsdrngilem  33721  qsdrngi  33722  rsprprmprmidlb  33758  rprmirredb  33767  1arithufdlem1  33779  1arithufdlem2  33780  1arithufdlem3  33781  1arithufdlem4  33782  fply1  33793  ply1degltel  33829  ply1degleel  33830  ply1degltlss  33831  mplmulmvr  33874  psrmon  33884  psrmonprod  33887  esplylem  33901  esplyfv1  33904  esplysply  33906  esplyind  33910  ply1degltdimlem  33957  ply1degltdim  33958  algextdeglem4  34055  algextdeglem6  34057  algextdeglem7  34058  algextdeglem8  34059  nn0constr  34096  smatlem  34132  smatcl  34137  zartopn  34210  zarmxt1  34215  tpr2rico  34247  xrmulc1cn  34265  xrge0mulc1cn  34276  esumpfinvallem  34409  ldgenpisyslem1  34498  dynkin  34502  brfae  34583  sxbrsigalem3  34607  dya2icoseg2  34613  omsmeas  34658  sibfof  34675  sseqmw  34726  sseqf  34727  sseqp1  34730  fiblem  34733  fibp1  34736  probfinmeasbALTV  34764  repr0  34943  reprpmtf1o  34958  hgt750lemg  34986  bnj1379  35163  srcmpltd  35413  fineqvnttrclselem3  35469  subfacp1lem5  35609  subfacp1lem6  35610  cvxpconn  35667  cvxsconn  35668  cvmliftlem6  35715  cvmliftlem8  35717  cvmliftlem10  35719  cvmlift2lem6  35733  cvmlift2lem11  35738  cvmlift2lem12  35739  2goelgoanfmla1  35849  prv1n  35856  msubff  35955  msubco  35956  elmsta  35973  msubff1  35981  mvhf  35983  msubvrs  35985  iprodefisumlem  36165  filnetlem3  36814  ttcid  36926  ttcwf  36958  knoppcnlem10  37014  knoppcnlem11  37015  icoreunrn  37927  icoreelrn  37929  ralssiun  37975  poimirlem3  38196  poimirlem16  38209  poimirlem17  38210  poimirlem19  38212  poimirlem30  38223  dvasin  38277  cover2  38288  upixp  38302  sdclem1  38316  fdc  38318  caushft  38334  ismtyres  38381  rrncmslem  38405  isfld2  38578  presuc  39071  osumcllem10N  40663  pexmidlem7N  40674  dihglblem2N  41992  lcfrvalsnN  42239  lcfrlem5  42244  lcfrlem6  42245  lcfrlem27  42267  lcfrlem37  42277  aks6d1c1p4  42802  aks6d1c1p7  42804  aks6d1c1p8  42806  evl1gprodd  42808  aks6d1c2lem4  42818  aks6d1c5lem3  42828  aks6d1c6lem2  42862  prjspvs  43268  0prjspnrel  43285  monotuz  43594  expdiophlem1  43674  kelac2  43718  naddwordnexlem4  44054  grurankcld  44883  dvgrat  44948  nzss  44953  uzmptshftfval  44982  binomcxplemnotnn0  44992  orbitinit  45591  orbitcl  45592  permaxinf2lem  45647  refsumcn  45676  rfcnpre2  45677  rfcnpre3  45679  rfcnpre4  45680  disjf1o  45835  unirnmap  45850  unirnmapsn  45856  ssmapsn  45858  mptssid  45882  allbutfi  46034  eluzd  46049  uzidd2  46056  ressiocsup  46196  ressioosup  46197  ressiooinf  46199  fsumsermpt  46221  climexp  46247  climinf  46248  climsuse  46250  sumnnodd  46272  limsupresico  46340  limsupubuzlem  46352  limsupresxr  46406  liminfresxr  46407  liminfresico  46411  limsup10exlem  46412  cnrefiisplem  46469  cncfiooicclem1  46533  dvsinax  46553  itgsinexplem1  46594  fvvolioof  46629  fvvolicof  46631  stoweidlem14  46654  stoweidlem16  46656  stoweidlem31  46671  stoweidlem34  46674  stoweidlem36  46676  stoweidlem43  46683  stoweidlem46  46686  stoweidlem47  46687  stoweidlem52  46692  stoweidlem55  46695  stoweidlem57  46697  dirkercncf  46747  fourierdlem20  46767  fourierdlem42  46789  fourierdlem51  46797  fourierdlem54  46800  fourierdlem62  46808  fourierdlem71  46817  fourierdlem80  46826  fourierdlem114  46860  fouriersw  46871  ioorrnopnlem  46944  ioorrnopnxrlem  46946  salexct3  46982  salgencntex  46983  salgensscntex  46984  subsalsal  46999  sge0fodjrnlem  47056  sge0isum  47067  sge0seq  47086  sge0reuz  47087  sge0reuzb  47088  meadjiunlem  47105  meaiininclem  47126  carageniuncllem1  47161  caratheodorylem1  47166  hoiprodp1  47228  hoidmv1lelem1  47231  hoidmv1lelem2  47232  hoidmv1le  47234  hoidmvlelem1  47235  hoidmvlelem2  47236  hoidmvlelem3  47237  voncmpl  47261  hoiqssbl  47265  smflimlem2  47412  smfsuplem1  47451  smfsuplem3  47453  fsupdm  47482  finfdm  47486  cfsetsnfsetf  47718  fcores  47727  afvres  47832  afv2res  47899  fundcmpsurinjimaid  48083  iccpartigtl  48095  sprsymrelf  48167  prproropf1olem2  48176  uhgrimedgi  48578  isuspgrim0lem  48581  isuspgrimlem  48583  ushggricedg  48615  grimedg  48623  usgrgrtrirex  48638  isubgr3stgrlem7  48660  uspgrlimlem4  48679  grlimprclnbgr  48684  gpgiedgdmellem  48734  gpg3kgrtriex  48777  funcringcsetcALTV2lem3  48980  funcringcsetclem3ALTV  49003  lindslinindsimp2lem5  49161  rrxsphere  49447  line2  49451  iooii  49615  icccldii  49616  iscnrm3rlem3  49639  eloppf2  49831  oppcup  49904  natoppf  49926  zeroo2  49931  oppfdiag1  50111  oppfdiag  50113  2arwcat  50297  incat  50298  lmddu  50364  onsetreclem3  50404  amgmwlem  50510