Theorem eqeltrrid 2837

Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)

Hypotheses

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

Assertion

Ref	Expression
eqeltrrid	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eqeltrrid

Step	Hyp	Ref	Expression
1		eqeltrrid.1	. . 3 ⊢ 𝐵 = 𝐴
2	1	eqcomi 2740	. 2 ⊢ 𝐴 = 𝐵
3		eqeltrrid.2	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
4	2, 3	eqeltrid 2836	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2809

This theorem is referenced by:  3eltr3g  2848  dmrnssfld  5969  oprssdm  7592  offval  7683  pwexr  7756  cnvexg  7919  resfunexgALT  7938  abrexexgOLD  7952  abrexex2g  7955  opabex3d  7956  opabex3rd  7957  frxp3  8141  suppssov1  8187  suppssfv  8191  ralxpmap  8894  unfi  9176  pwfir  9180  pwfilem  9181  residfi  9337  imafiALT  9349  abrexfi  9356  ssfii  9418  wdomima2g  9585  unxpwdom2  9587  tskwe  9949  ac10ct  10033  fin23lem28  10339  fin23lem30  10341  axcclem  10456  distrlem4pr  11025  iccshftr  13468  iccshftl  13470  iccdil  13472  icccntr  13474  o1res  15509  exprmfct  16646  infpnlem1  16848  4sqlem13  16895  0ram  16958  ressval3d  17196  ressval3dOLD  17197  ismred2  17552  mreexexlem2d  17594  mreexexlem4d  17596  acsfn1c  17611  acsfn2  17612  ssclem  17771  submacs  18745  symgtset  19309  symgsubmefmndALT  19313  efgrcl  19625  cntrcmnd  19752  cntrabl  19753  dprd2da  19954  srgbinom  20126  irredlmul  20320  rngridlmcl  20984  lidlrsppropd  21005  rngqiprngghmlem1  21047  rngqiprnglinlem2  21052  rngqiprngimf1lem  21054  rngqiprng  21056  rngqiprngimf  21057  rngqiprngghm  21059  rngqiprngimf1  21060  rngqiprngimfo  21061  rng2idl1cntr  21065  rngqiprngfulem4  21074  rngqipring1  21076  pzriprnglem6  21256  chrcl  21298  css1  21463  issubassa  21641  ply1crng  21942  ply1ring  21991  ply1lmod  21995  oftpos  22175  tposmap  22180  0opn  22627  fctop2  22729  difopn  22759  tgrest  22884  ordtbas2  22916  ordtopn3  22921  ordtcld3  22924  t1ficld  23052  resthauslem  23088  kgentopon  23263  txbasex  23291  txcnpi  23333  txdis1cn  23360  pthaus  23363  txkgen  23377  cnmptid  23386  cnmptc  23387  cnmpt1st  23393  cnmpt2nd  23394  cnmpt2c  23395  cnmptkc  23404  txconn  23414  hmeoima  23490  hmeocld  23492  xkohmeo  23540  filufint  23645  fin1aufil  23657  flftg  23721  ptcmplem2  23778  tmdmulg  23817  tmdgsum2  23821  submtmd  23829  symgtgp  23831  ghmcnp  23840  qustgpopn  23845  qustgplem  23846  ust0  23945  nrginvrcn  24430  fsumcn  24609  fsum2cn  24610  expcn  24611  expcnOLD  24613  cnheibor  24702  evth2  24707  csscld  24998  clsocv  24999  ovoliun2  25256  volfiniun  25297  dyadmbl  25350  mbfeqalem2  25392  mbfss  25396  ismbf3d  25404  mbfadd  25411  i1f0rn  25432  mbfmul  25477  itg2seq  25493  itg2monolem2  25502  itg2monolem3  25503  itg2mono  25504  itgreval  25547  itgge0  25561  itgss3  25565  iblconst  25568  itgconst  25569  ibladdlem  25570  itgfsum  25577  iblabslem  25578  itgabs  25585  lhop1lem  25766  dvfsumle  25774  dvfsumlem2  25780  ftc1lem4  25792  itgparts  25800  itgsubstlem  25801  itgsubst  25802  plydivlem1  26043  aannenlem1  26078  taylply2  26117  itgulm  26157  cxpcn  26490  resqrtcn  26494  basellem1  26822  mulogsumlem  27271  mulog2sumlem2  27275  selberg2lem  27290  pntrsumo1  27305  addsuniflem  27724  ssltmul1  27842  ssltmul2  27843  precsexlem11  27903  usgrnbcnvfv  28890  ewlksfval  29126  crctcshwlkn0  29343  pjssmii  31202  abrexexd  32014  mptiffisupp  32183  pfxlsw2ccat  32384  cntrcrng  32485  ogrpaddltrbid  32509  ply1degltdimlem  32996  lmatfval  33093  pl1cn  33234  esumcvg  33383  esumcvgsum  33385  sigaval  33408  sigaclfu2  33418  sigapildsys  33459  ldgenpisys  33463  measinb2  33520  braew  33539  unelcarsg  33610  carsgclctunlem2  33617  sibfof  33638  sitgclg  33640  orrvcoel  33763  orrvccel  33764  fsum2dsub  33918  fineqvpow  34395  subfaclefac  34466  cvmsss2  34564  cvmopnlem  34568  satf0suclem  34665  mpstrcl  34831  elmpps  34863  gg-cmvth  35467  gg-dvfsumle  35469  gg-dvfsumlem2  35470  gg-cxpcn  35471  hmeoclda  35522  bj-1uplex  36193  bj-2uplex  36207  icoreclin  36542  broucube  36826  mblfinlem1  36829  cnambfre  36840  ibladdnclem  36848  iblabsnclem  36855  itgabsnc  36861  ftc1cnnclem  36863  ftc1anclem4  36868  ftc1anclem5  36869  ftc1anclem6  36870  ftc1anclem7  36871  ftc2nc  36874  areacirc  36885  zrdivrng  37125  xrnresex  37580  dalemrot  38832  dalem10  38848  arglem1N  39365  cdlemk36  40088  resopunitintvd  41198  resclunitintvd  41199  lcmineqlem2  41202  mzpconstmpt  41781  mzpresrename  41791  diophrex  41816  0dioph  41819  anrabdioph  41821  orrabdioph  41822  rabren3dioph  41856  dvradcnv2  43409  xpexb  43516  fsumcnf  44008  uzublem  44439  fprodcncf  44915  iblconstmpt  44971  itgiccshift  44995  itgperiod  44996  itgsbtaddcnst  44997  dirkercncflem2  45119  fourierdlem47  45168  saluni  45340  sge0iunmpt  45433  sge0xaddlem2  45449  sge0xadd  45450  hoidmvlelem3  45612  ctvonmbl  45704  vonct  45708  smfaddlem2  45779  smfmullem4  45809  singoutnword  45895  aoprssdm  46209