Theorem eleqtrrdi 2874

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838

This theorem is referenced by:  3eltr4g  2880  brelrng  5931  elabrex  7240  elabrexg  7241  fliftel1  7308  ovidig  7552  unielxp  8020  tfrlem11  8371  rdglim  8409  seqomlem4  8436  2oconcl  8484  ecopqsi  8764  erov  8808  eroprf  8809  sbthlem2  9072  dffi3  9387  ixpiunwdom  9548  cantnfcl  9632  r1lim  9740  rankwflemb  9761  pwwf  9775  unwf  9778  rankwflem  9783  uniwf  9787  rankpwi  9791  rankr1g  9800  r1pw  9813  r1rankid  9827  rankuni  9831  djulcl  9892  djurcl  9893  inlresf  9896  inrresf  9898  djuun  9908  cardlim  9954  infxpenlem  9993  alephfp  10088  cfsmolem  10249  alephsing  10255  hsmexlem4  10408  axdc3lem2  10430  numth3  10449  iunfo  10518  konigthlem  10548  iunctb  10554  canthwelem  10630  canthwe  10631  r1limwun  10716  inar1  10755  inatsk  10758  gruina  10798  grur1  10800  tskmval  10819  tskmcl  10821  pinq  10907  dmrecnq  10948  addclsr  11063  mulclsr  11064  axaddf  11125  axmulf  11126  peano2nn  12240  uztrn2  12876  eluz2nn  12907  peano2uzs  12921  uzsupss  12959  uzsup  13892  uzrdgfni  13990  uzrdgsuci  13992  fsuppmapnn0fiub  14023  seqf  14055  ser0  14086  bcm1k  14347  bcp1nk  14349  bcpasc  14353  hashprdifel  14430  fz1isolem  14494  pr2pwpr  14512  tpf  14532  ccats1val2  14661  rexuzre  15400  limsupgre  15528  climconst  15590  rlimclim1  15592  climrlim2  15594  clim2ser  15702  clim2ser2  15703  iserex  15704  isermulc2  15705  iserle  15707  isercolllem3  15714  isercoll2  15716  climsup  15717  iseraltlem2  15730  iseraltlem3  15731  zsum  15765  isumclim3  15806  isumadd  15814  fsump1i  15816  iserabs  15863  cvgcmp  15864  cvgcmpub  15865  cvgcmpce  15866  abscvgcvg  15867  isumshft  15889  isumsplit  15890  isum1p  15891  isumrpcl  15893  isumsup2  15896  climcndslem1  15899  cvgrat  15933  clim2prod  15938  clim2div  15939  prodf1  15941  ntrivcvgn0  15948  ntrivcvgtail  15950  fprodntriv  15992  fprodabs  16024  fprodeq0  16025  iprodclim3  16050  iprodmul  16053  ef0lem  16127  fprodefsum  16144  rpnnen2lem3  16267  dvdsflip  16370  fzo0dvdseq  16376  bitsinv1  16495  smupval  16541  smueqlem  16543  seq1st  16624  algr0  16625  prmind2  16738  crth  16832  eulerthlem2  16836  prmdiv  16839  pockthlem  16960  pockthg  16961  unbenlem  16963  prmunb  16969  prmgaplem7  17112  strfv2d  17256  imasvscaval  17587  oppccatid  17770  oppccatf  17779  epii  17795  fthepi  17982  funcestrcsetclem3  18193  funcsetcestrclem3  18207  yon12  18316  yon2  18317  yonedalem4c  18328  yonedalem22  18329  yonedalem3b  18330  yonedainv  18332  acsmapd  18605  chnub  18673  chnccats1  18676  chnccat  18677  mgm2nsgrplem1  18975  mgm2nsgrplem2  18976  mgm2nsgrplem3  18977  sgrp2nmndlem1  18980  sgrp2rid2  18983  ghmqusker  19352  cntrsubgnsg  19408  symgpssefmnd  19461  pmtrrn  19522  gexcl3  19652  efgi  19784  efgi2  19790  efgs1b  19801  efgredlemg  19807  efgredlemd  19809  frgpnabllem1  19938  cycsubgcyg  19966  gsumzaddlem  19986  dprdwd  20078  dprd2da  20109  rhmopp  20606  lsppratlem3  21273  lsppratlem4  21274  lbsextlem2  21283  lidl0ALT  21354  lidl1ALT  21357  2idl0  21399  2idl1  21400  rhmpreimaprmidl  21479  ssdifidllem  21484  ssdifidl  21485  domnchr  21682  znf1o  21701  mplsubrglem  22153  mpfconst  22260  mpfproj  22261  mpfind  22266  mhpmulcl  22312  pf1const  22506  pf1id  22507  mpfpf1  22511  pf1mpf  22512  madetsumid  22618  slesolex  22839  pmatcoe1fsupp  22858  mat2pmatbas0  22884  pmatcollpw  22938  pm2mpf1  22956  isclo  23244  indiscld  23248  restntr  23339  ordtbaslem  23345  ordtbas2  23348  lmconst  23418  lmss  23455  conncompid  23588  2ndcomap  23615  locfincmp  23683  comppfsc  23689  xkouni  23756  txcls  23761  ptclsg  23772  uptx  23782  txindis  23791  tx1stc  23807  cnmpt1res  23833  tgqtop  23869  uffix  24078  cnpflf2  24157  ptcmplem2  24210  ptcmplem4  24212  tgpconncomp  24270  tsmsfbas  24285  fmucnd  24448  prdsxmetlem  24525  imasdsf1olem  24530  prdsbl  24648  blcvx  24955  xrsmopn  24970  xrge0tsms  24992  metdcn2  24997  expcncf  25085  cnmpopc  25087  icchmeo  25100  iccpnfhmeo  25104  cnheibor  25114  evth  25118  evth2  25119  lebnumlem2  25121  lebnumii  25125  reparphti  25156  cfilfcls  25433  minveclem2  25585  minveclem3  25588  minveclem4  25591  ovoliunlem1  25661  ovolicc1  25675  iundisj  25707  volsup  25715  uniioombllem3  25744  vitalilem2  25768  vitalilem3  25769  mbfsup  25823  mbfinf  25824  mbflimsup  25825  itg2monolem1  25909  limcflflem  26039  limccnp  26050  limccnp2  26051  dvidlem  26074  dvn2bss  26089  cpnres  26096  dvcobr  26105  dvrec  26114  c1liplem1  26155  dvcnvrelem2  26177  dvfsumrlimf  26184  dvfsumlem1  26185  dvfsumlem2  26186  dvfsumlem3  26187  dvfsumlem4  26188  dvfsumrlim  26190  dvfsum2  26193  coeeulem  26381  coeid3  26397  plycn  26418  dvntaylp  26534  taylthlem1  26536  taylthlem2  26537  ulm2  26548  ulmshftlem  26552  ulmshft  26553  ulm0  26554  ulmcn  26562  ulmdvlem3  26565  ulmdv  26566  mtest  26567  mtestbdd  26568  dvradcnv  26584  psercn2  26586  psercn  26589  pserdv  26592  abelth  26604  efif1olem2  26708  efif1olem4  26710  efifo  26712  eff1olem  26713  logcn  26812  dvloglem  26813  cxpcn3  26913  resqrtcn  26914  sqrtcn  26915  logbleb  26948  logblt  26949  asinneg  27051  atanlogsub  27081  atanbnd  27091  ressatans  27099  leibpilem2  27106  xrlimcnp  27133  efrlim  27134  scvxcvx  27150  ppiub  27368  chtub  27376  logexprlim  27389  lgseisenlem1  27539  rplogsumlem1  27648  rplogsumlem2  27649  dchrisumlem2  27654  dchrisum0flb  27674  logdivbnd  27720  pntlem3  27773  dfnns2  28565  tgcgr4  28800  ltgov  28866  f1otrg  29220  eengtrkg  29336  iedgedg  29400  ushgredgedgloop  29581  subgruhgredgd  29634  uvtxupgrres  29758  umgr2v2evd2  29877  edginwlk  29984  wlk1walk  29988  crctcshwlkn0lem6  30164  wlkiswwlks1  30216  minvecolem1  31226  minvecolem2  31227  minvecolem4  31232  htthlem  31269  5oalem2  32007  3oalem2  32015  iundisjf  32934  fmptco1f1o  32978  xppreima  32990  xppreima2  32996  dfcnv2  33020  ccatws1f1o  33271  gsumhashmul  33387  xrge0tsmsd  33393  gsumwrd2dccatlem  33397  odpmco  33406  pmtrcnelor  33411  fzo0pmtrlast  33412  wrdpmtrlast  33413  pmtrto1cl  33419  psgnfzto1stlem  33420  fzto1stfv1  33421  fzto1st  33423  fzto1stinvn  33424  psgnfzto1st  33425  tocycf  33437  cycpmco2lem7  33452  cycpmco2  33453  cycpmrn  33463  cyc3evpm  33470  cyc3genpmlem  33471  cycpmgcl  33473  cyc3conja  33477  elrgspnlem1  33562  elrgspnlem2  33563  elrgspnlem3  33564  elrgspnlem4  33565  elrgspnsubrunlem1  33567  nsgmgc  33721  nsgqusf1olem1  33722  nsgqusf1olem2  33723  ssmxidllem  33756  drngmxidlr  33760  opprqus1r  33774  qsdrngilem  33776  qsdrngi  33777  rsprprmprmidlb  33813  rprmirredb  33822  1arithufdlem1  33834  1arithufdlem2  33835  1arithufdlem3  33836  1arithufdlem4  33837  fply1  33848  ply1degltel  33884  ply1degleel  33885  ply1degltlss  33886  mplmulmvr  33929  psrmon  33939  psrmonprod  33942  esplylem  33956  esplyfv1  33959  esplysply  33961  esplyind  33965  ply1degltdimlem  34012  ply1degltdim  34013  algextdeglem4  34110  algextdeglem6  34112  algextdeglem7  34113  algextdeglem8  34114  nn0constr  34151  smatlem  34187  smatcl  34192  zartopn  34265  zarmxt1  34270  tpr2rico  34302  xrmulc1cn  34320  xrge0mulc1cn  34331  esumpfinvallem  34464  ldgenpisyslem1  34553  dynkin  34557  brfae  34638  sxbrsigalem3  34662  dya2icoseg2  34668  omsmeas  34713  sibfof  34730  sseqmw  34781  sseqf  34782  sseqp1  34785  fiblem  34788  fibp1  34791  probfinmeasbALTV  34819  repr0  34998  reprpmtf1o  35013  hgt750lemg  35041  bnj1379  35218  srcmpltd  35469  fineqvnttrclselem3  35536  subfacp1lem5  35676  subfacp1lem6  35677  cvxpconn  35734  cvxsconn  35735  cvmliftlem6  35782  cvmliftlem8  35784  cvmliftlem10  35786  cvmlift2lem6  35800  cvmlift2lem11  35805  cvmlift2lem12  35806  2goelgoanfmla1  35916  prv1n  35923  msubff  36022  msubco  36023  elmsta  36040  msubff1  36048  mvhf  36050  msubvrs  36052  iprodefisumlem  36232  filnetlem3  36911  ttcid  37023  ttcwf  37055  knoppcnlem10  37111  knoppcnlem11  37112  icoreunrn  38025  icoreelrn  38027  ralssiun  38073  poimirlem3  38294  poimirlem16  38307  poimirlem17  38308  poimirlem19  38310  poimirlem30  38321  dvasin  38375  cover2  38386  upixp  38400  sdclem1  38414  fdc  38416  caushft  38432  ismtyres  38479  rrncmslem  38503  isfld2  38676  presuc  39167  osumcllem10N  40759  pexmidlem7N  40770  dihglblem2N  42088  lcfrvalsnN  42335  lcfrlem5  42340  lcfrlem6  42341  lcfrlem27  42363  lcfrlem37  42373  aks6d1c1p4  42898  aks6d1c1p7  42900  aks6d1c1p8  42902  evl1gprodd  42904  aks6d1c2lem4  42914  aks6d1c5lem3  42924  aks6d1c6lem2  42958  prjspvs  43362  0prjspnrel  43379  monotuz  43688  expdiophlem1  43768  kelac2  43812  naddwordnexlem4  44148  grurankcld  44977  dvgrat  45042  nzss  45047  uzmptshftfval  45076  binomcxplemnotnn0  45086  orbitinit  45685  orbitcl  45686  permaxinf2lem  45741  refsumcn  45770  rfcnpre2  45771  rfcnpre3  45773  rfcnpre4  45774  disjf1o  45929  unirnmap  45944  unirnmapsn  45950  ssmapsn  45952  mptssid  45976  allbutfi  46128  eluzd  46143  uzidd2  46150  ressiocsup  46290  ressioosup  46291  ressiooinf  46293  fsumsermpt  46315  climexp  46341  climinf  46342  climsuse  46344  sumnnodd  46366  limsupresico  46434  limsupubuzlem  46446  limsupresxr  46500  liminfresxr  46501  liminfresico  46505  limsup10exlem  46506  cnrefiisplem  46563  cncfiooicclem1  46627  dvsinax  46647  itgsinexplem1  46688  fvvolioof  46723  fvvolicof  46725  stoweidlem14  46748  stoweidlem16  46750  stoweidlem31  46765  stoweidlem34  46768  stoweidlem36  46770  stoweidlem43  46777  stoweidlem46  46780  stoweidlem47  46781  stoweidlem52  46786  stoweidlem55  46789  stoweidlem57  46791  dirkercncf  46841  fourierdlem20  46861  fourierdlem42  46883  fourierdlem51  46891  fourierdlem54  46894  fourierdlem62  46902  fourierdlem71  46911  fourierdlem80  46920  fourierdlem114  46954  fouriersw  46965  ioorrnopnlem  47038  ioorrnopnxrlem  47040  salexct3  47076  salgencntex  47077  salgensscntex  47078  subsalsal  47093  sge0fodjrnlem  47150  sge0isum  47161  sge0seq  47180  sge0reuz  47181  sge0reuzb  47182  meadjiunlem  47199  meaiininclem  47220  carageniuncllem1  47255  caratheodorylem1  47260  hoiprodp1  47322  hoidmv1lelem1  47325  hoidmv1lelem2  47326  hoidmv1le  47328  hoidmvlelem1  47329  hoidmvlelem2  47330  hoidmvlelem3  47331  voncmpl  47355  hoiqssbl  47359  smflimlem2  47506  smfsuplem1  47545  smfsuplem3  47547  fsupdm  47576  finfdm  47580  cfsetsnfsetf  47815  fcores  47824  afvres  47929  afv2res  47996  fundcmpsurinjimaid  48180  iccpartigtl  48192  sprsymrelf  48264  prproropf1olem2  48273  uhgrimedgi  48675  isuspgrim0lem  48678  isuspgrimlem  48680  ushggricedg  48712  grimedg  48720  usgrgrtrirex  48735  isubgr3stgrlem7  48757  uspgrlimlem4  48776  grlimprclnbgr  48781  gpgiedgdmellem  48831  gpg3kgrtriex  48874  funcringcsetcALTV2lem3  49077  funcringcsetclem3ALTV  49100  lindslinindsimp2lem5  49262  rrxsphere  49548  line2  49552  iooii  49716  icccldii  49717  iscnrm3rlem3  49740  eloppf2  49932  oppcup  50005  natoppf  50027  zeroo2  50032  oppfdiag1  50212  oppfdiag  50214  2arwcat  50398  incat  50399  lmddu  50465  onsetreclem3  50505  amgmwlem  50669