Theorem eleqtrrdi 2872

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

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

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-clel 2836

This theorem is used by:  3eltr4g  2878  srcmpltd  4432  brelrng  5923  elabrex  7246  elabrexg  7247  fliftel1  7318  ovidig  7562  unielxp  8039  tfrlem11  8396  rdglim  8434  seqomlem4  8463  2oconcl  8511  ecopqsi  8791  erov  8835  eroprf  8836  sbthlem2  9107  dffi3  9423  ixpiunwdom  9584  cantnfcl  9668  r1lim  9779  rankwflembOLD  9801  pwwf  9815  unwf  9818  rankwflem  9824  uniwf  9828  rankpwi  9832  rankr1g  9844  r1pw  9859  r1rankid  9875  rankuni  9879  elhf4  9912  djulcl  9991  djurcl  9992  inlresf  9995  inrresf  9997  djuun  10007  cardlim  10053  infxpenlem  10092  alephfp  10187  cfsmolem  10348  alephsing  10354  hsmexlem4  10507  axdc3lem2  10529  numth3  10548  iunfo  10623  konigthlem  10653  iunctb  10659  canthwelem  10735  canthwe  10736  r1limwun  10821  inar1  10860  inatsk  10863  gruina  10903  grur1  10905  tskmval  10924  tskmcl  10926  pinq  11012  dmrecnq  11053  addclsr  11168  mulclsr  11169  axaddf  11230  axmulf  11231  peano2nn  12347  uztrn2  12984  eluz2nn  13015  peano2uzs  13029  uzsupss  13067  uzsup  14003  uzrdgfni  14101  uzrdgsuci  14103  fsuppmapnn0fiub  14134  seqf  14166  ser0  14197  bcm1k  14459  bcp1nk  14461  bcpasc  14465  hashprdifel  14542  fz1isolem  14606  pr2pwpr  14624  tpf  14644  ccats1val2  14775  rexuzre  15520  limsupgre  15648  climconst  15710  rlimclim1  15712  climrlim2  15714  clim2ser  15822  clim2ser2  15823  iserex  15824  isermulc2  15825  iserle  15827  isercolllem3  15834  isercoll2  15836  climsup  15837  iseraltlem2  15850  iseraltlem3  15851  zsum  15884  isumclim3  15925  isumadd  15933  fsump1i  15935  iserabs  15982  cvgcmp  15983  cvgcmpub  15984  cvgcmpce  15985  abscvgcvg  15986  isumshft  16008  isumsplit  16009  isum1p  16010  isumrpcl  16012  isumsup2  16015  climcndslem1  16018  cvgrat  16052  clim2prod  16057  clim2div  16058  prodf1  16060  ntrivcvgn0  16067  ntrivcvgtail  16069  fprodntriv  16109  fprodabs  16141  fprodeq0  16142  iprodclim3  16167  iprodmul  16170  ef0lem  16244  fprodefsum  16261  rpnnen2lem3  16384  dvdsflip  16487  fzo0dvdseq  16493  bitsinv1  16612  smupval  16658  smueqlem  16660  seq1st  16746  algr0  16747  prmind2  16860  crth  16955  eulerthlem2  16959  prmdiv  16962  pockthlem  17083  pockthg  17084  unbenlem  17086  prmunb  17092  prmgaplem7  17235  strfv2d  17379  imasvscaval  17710  oppccatid  17893  oppccatf  17902  epii  17918  fthepi  18105  funcestrcsetclem3  18316  funcsetcestrclem3  18330  yon12  18439  yon2  18440  yonedalem4c  18451  yonedalem22  18452  yonedalem3b  18453  yonedainv  18455  acsmapd  18728  chnub  18796  chnccats1  18799  chnccat  18800  mgm2nsgrplem1  19117  mgm2nsgrplem2  19118  mgm2nsgrplem3  19119  sgrp2nmndlem1  19122  sgrp2rid2  19125  ghmqusker  19501  cntrsubgnsg  19557  symgpssefmnd  19610  pmtrrn  19671  gexcl3  19801  efgi  19933  efgi2  19939  efgs1b  19950  efgredlemg  19956  efgredlemd  19958  frgpnabllem1  20087  cycsubgcyg  20115  gsumzaddlem  20135  dprdwd  20227  dprd2da  20258  rhmopp  20759  lsppratlem3  21427  lsppratlem4  21428  lbsextlem2  21437  lidl0ALT  21508  lidl1ALT  21511  2idl0  21554  2idl1  21555  rhmpreimaprmidl  21635  ssdifidllem  21640  ssdifidl  21641  domnchr  21838  znf1o  21857  mplsubrglem  22311  mpfconst  22418  mpfproj  22419  mpfind  22424  mhpmulcl  22470  pf1const  22664  pf1id  22665  mpfpf1  22669  pf1mpf  22670  madetsumid  22776  slesolex  23000  pmatcoe1fsupp  23019  mat2pmatbas0  23045  pmatcollpw  23099  pm2mpf1  23117  isclo  23405  indiscld  23409  restntr  23500  ordtbaslem  23506  ordtbas2  23509  lmconst  23579  lmss  23616  conncompid  23749  2ndcomap  23777  locfincmp  23845  comppfsc  23851  xkouni  23918  txcls  23923  ptclsg  23934  uptx  23944  txindis  23953  tx1stc  23969  cnmpt1res  23995  tgqtop  24031  uffix  24240  cnpflf2  24319  ptcmplem2  24372  ptcmplem4  24374  tgpconncomp  24432  tsmsfbas  24447  fmucnd  24610  prdsxmetlem  24687  imasdsf1olem  24692  prdsbl  24810  blcvx  25117  xrsmopn  25132  xrge0tsms  25154  metdcn2  25159  expcncf  25247  cnmpopc  25249  icchmeo  25262  iccpnfhmeo  25266  cnheibor  25276  evth  25280  evth2  25281  lebnumlem2  25283  lebnumii  25287  reparphti  25318  cfilfcls  25595  minveclem2  25747  minveclem3  25750  minveclem4  25753  ovoliunlem1  25823  ovolicc1  25837  iundisj  25869  volsup  25877  uniioombllem3  25906  vitalilem2  25930  vitalilem3  25931  mbfsup  25985  mbfinf  25986  mbflimsup  25987  itg2monolem1  26071  limcflflem  26200  limccnp  26211  limccnp2  26212  dvidlem  26235  dvn2bss  26250  cpnres  26257  dvcobr  26266  dvrec  26275  c1liplem1  26316  dvcnvrelem2  26338  dvfsumrlimf  26345  dvfsumlem1  26346  dvfsumlem2  26347  dvfsumlem3  26348  dvfsumlem4  26349  dvfsumrlim  26351  dvfsum2  26354  coeeulem  26543  coeid3  26559  plycn  26580  dvntaylp  26698  taylthlem1  26700  taylthlem2  26701  ulm2  26712  ulmshftlem  26716  ulmshft  26717  ulm0  26718  ulmcn  26726  ulmdvlem3  26729  ulmdv  26730  mtest  26731  mtestbdd  26732  dvradcnv  26748  psercn2  26750  psercn  26753  pserdv  26756  abelth  26768  efif1olem2  26871  efif1olem4  26873  efifo  26875  eff1olem  26876  logcn  26975  dvloglem  26976  cxpcn3  27076  resqrtcn  27077  sqrtcn  27078  logbleb  27111  logblt  27112  asinneg  27214  atanlogsub  27244  atanbnd  27254  ressatans  27262  leibpilem2  27269  xrlimcnp  27296  efrlim  27297  scvxcvx  27313  ppiub  27531  chtub  27539  logexprlim  27552  lgseisenlem1  27702  rplogsumlem1  27811  rplogsumlem2  27812  dchrisumlem2  27817  dchrisum0flb  27837  logdivbnd  27883  pntlem3  27936  dfnns2  28758  tgcgr4  28994  ltgov  29060  elcgrabasrd  29376  cgrabasimass  29378  f1otrg  29448  eengtrkg  29564  iedgedg  29628  ushgredgedgloop  29812  subgruhgredgd  29865  uvtxupgrres  29989  umgr2v2evd2  30108  edginwlk  30215  wlk1walk  30219  crctcshwlkn0lem6  30404  wlkiswwlks1  30456  minvecolem1  31476  minvecolem2  31477  minvecolem4  31482  htthlem  31519  5oalem2  32257  3oalem2  32265  iundisjf  33183  fmptco1f1o  33227  xppreima  33239  xppreima2  33245  dfcnv2  33269  ccatws1f1o  33514  gsumhashmul  33628  xrge0tsmsd  33634  gsumwrd2dccatlem  33638  odpmco  33647  pmtrcnelor  33652  fzo0pmtrlast  33653  wrdpmtrlast  33654  pmtrto1cl  33660  psgnfzto1stlem  33661  fzto1stfv1  33662  fzto1st  33664  fzto1stinvn  33665  psgnfzto1st  33666  tocycf  33678  cycpmco2lem7  33693  cycpmco2  33694  cycpmrn  33704  cyc3evpm  33711  cyc3genpmlem  33712  cycpmgcl  33714  cyc3conja  33718  elrgspnlem1  33803  elrgspnlem2  33804  elrgspnlem3  33805  elrgspnlem4  33806  elrgspnsubrunlem1  33808  nsgmgc  33963  nsgqusf1olem1  33964  nsgqusf1olem2  33965  ssmxidllem  33998  drngmxidlr  34002  opprqus1r  34016  qsdrngilem  34018  qsdrngi  34019  rsprprmprmidlb  34055  rprmirredb  34064  1arithufdlem1  34076  1arithufdlem2  34077  1arithufdlem3  34078  1arithufdlem4  34079  fply1  34090  ply1degltel  34126  ply1degleel  34127  ply1degltlss  34128  mplmulmvr  34171  psrmon  34181  psrmonprod  34184  esplylem  34198  esplyfv1  34201  esplysply  34203  esplyind  34207  ply1degltdimlem  34254  ply1degltdim  34255  algextdeglem4  34352  algextdeglem6  34354  algextdeglem7  34355  algextdeglem8  34356  nn0constr  34393  smatlem  34429  smatcl  34434  zartopn  34507  zarmxt1  34512  tpr2rico  34544  xrmulc1cn  34562  xrge0mulc1cn  34573  esumpfinvallem  34706  ldgenpisyslem1  34796  dynkin  34800  brfae  34881  sxbrsigalem3  34904  dya2icoseg2  34910  omsmeas  34955  sibfof  34972  sseqmw  35023  sseqf  35024  sseqp1  35027  fiblem  35030  fibp1  35033  probfinmeasbALTV  35061  repr0  35240  reprpmtf1o  35255  hgt750lemg  35283  bnj1379  35460  fineqvnttrclselem3  35791  subfacp1lem5  35949  subfacp1lem6  35950  cvxpconn  36007  cvxsconn  36008  cvmliftlem6  36055  cvmliftlem8  36057  cvmliftlem10  36059  cvmlift2lem6  36073  cvmlift2lem11  36078  cvmlift2lem12  36079  2goelgoanfmla1  36189  prv1n  36196  msubff  36295  msubco  36296  elmsta  36313  msubff1  36321  mvhf  36323  msubvrs  36325  iprodefisumlem  36505  filnetlem3  37168  ttcid  37280  ttcwf  37312  knoppcnlem10  37368  knoppcnlem11  37369  icoreunrn  38282  icoreelrn  38284  ralssiun  38330  poimirlem3  38541  poimirlem16  38554  poimirlem17  38555  poimirlem19  38557  poimirlem30  38568  dvasin  38622  varprop  38642  negprop  38643  impprop  38644  cover2  38649  upixp  38663  sdclem1  38677  fdc  38679  caushft  38695  ismtyres  38742  rrncmslem  38766  isfld2  38939  presuc  39430  osumcllem10N  41022  pexmidlem7N  41033  dihglblem2N  42351  lcfrvalsnN  42598  lcfrlem5  42603  lcfrlem6  42604  lcfrlem27  42626  lcfrlem37  42636  aks6d1c1p4  43161  aks6d1c1p7  43163  aks6d1c1p8  43165  evl1gprodd  43167  aks6d1c2lem4  43177  aks6d1c5lem3  43187  aks6d1c6lem2  43221  prjspvs  43638  frlmnzcoordsca  43658  prjspnnorm  43661  0prjspnrel  43663  monotuz  43947  expdiophlem1  44027  kelac2  44066  naddwordnexlem4  44402  grurankcld  45230  dvgrat  45295  nzss  45300  uzmptshftfval  45329  binomcxplemnotnn0  45339  orbitinit  45945  orbitcl  45946  permaxinf2lem  46001  ishfstruct  46027  refsumcn  46046  rfcnpre2  46047  rfcnpre3  46049  rfcnpre4  46050  disjf1o  46205  unirnmap  46220  unirnmapsn  46226  ssmapsn  46228  mptssid  46252  allbutfi  46403  eluzd  46418  uzidd2  46425  ressiocsup  46565  ressioosup  46566  ressiooinf  46568  fsumsermpt  46590  climexp  46616  climinf  46617  climsuse  46619  limsupresico  46709  limsupubuzlem  46721  limsupresxr  46775  liminfresxr  46776  liminfresico  46780  limsup10exlem  46781  cnrefiisplem  46838  cncfiooicclem1  46902  dvsinax  46922  itgsinexplem1  46963  fvvolioof  46998  fvvolicof  47000  stoweidlem14  47023  stoweidlem16  47025  stoweidlem31  47040  stoweidlem34  47043  stoweidlem36  47045  stoweidlem43  47052  stoweidlem46  47055  stoweidlem47  47056  stoweidlem52  47061  stoweidlem55  47064  stoweidlem57  47066  dirkercncf  47116  fourierdlem20  47136  fourierdlem42  47158  fourierdlem51  47166  fourierdlem54  47169  fourierdlem62  47177  fourierdlem71  47186  fourierdlem80  47195  fourierdlem114  47229  fouriersw  47240  ioorrnopnlem  47313  ioorrnopnxrlem  47315  salexct3  47351  salgencntex  47352  salgensscntex  47353  subsalsal  47368  sge0fodjrnlem  47425  sge0isum  47436  sge0seq  47455  sge0reuz  47456  sge0reuzb  47457  meadjiunlem  47474  meaiininclem  47495  carageniuncllem1  47530  caratheodorylem1  47535  hoiprodp1  47597  hoidmv1lelem1  47600  hoidmv1lelem2  47601  hoidmv1le  47603  hoidmvlelem1  47604  hoidmvlelem2  47605  hoidmvlelem3  47606  voncmpl  47630  hoiqssbl  47634  smflimlem2  47781  smfsuplem1  47820  smfsuplem3  47822  fsupdm  47851  finfdm  47855  sinnpoly  47940  cfsetsnfsetf  48127  fcores  48136  afvres  48241  afv2res  48308  fundcmpsurinjimaid  48492  iccpartigtl  48504  sprsymrelf  48576  prproropf1olem2  48585  uhgrimedgi  48987  isuspgrim0lem  48990  isuspgrimlem  48992  ushggricedg  49024  grimedg  49032  usgrgrtrirex  49047  isubgr3stgrlem7  49069  uspgrlimlem4  49088  grlimprclnbgr  49093  gpgiedgdmellem  49143  gpg3kgrtriex  49186  funcringcsetcALTV2lem3  49388  funcringcsetclem3ALTV  49411  lindslinindsimp2lem5  49573  rrxsphere  49859  line2  49863  iooii  50025  icccldii  50026  iscnrm3rlem3  50049  eloppf2  50241  oppcup  50314  natoppf  50336  zeroo2  50341  oppfdiag1  50521  oppfdiag  50523  2arwcat  50707  incat  50708  lmddu  50774  onsetreclem3  50799  amgmwlem  50986