Theorem eqeltrrid 2836

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 2835	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111

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 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

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

This theorem is referenced by:  3eltr3g  2847  dmrnssfld  5918  oprssdm  7533  offval  7625  pwexr  7704  cnvexg  7860  resfunexgALT  7886  abrexex2g  7902  opabex3d  7903  opabex3rd  7904  frxp3  8087  suppssov1  8133  suppssov2  8134  suppssfv  8138  ralxpmap  8826  unfi  9086  imafi  9205  pwfir  9207  pwfilem  9208  residfi  9228  abrexfi  9242  ssfii  9309  wdomima2g  9478  unxpwdom2  9480  tskwe  9849  ac10ct  9931  fin23lem28  10237  fin23lem30  10239  axcclem  10354  distrlem4pr  10923  iccshftr  13392  iccshftl  13394  iccdil  13396  icccntr  13398  o1res  15473  exprmfct  16621  infpnlem1  16828  4sqlem13  16875  0ram  16938  ressval3d  17163  ismred2  17511  mreexexlem2d  17557  mreexexlem4d  17559  acsfn1c  17574  acsfn2  17575  ssclem  17732  submacs  18741  symgtset  19317  symgsubmefmndALT  19321  efgrcl  19633  cntrcmnd  19760  cntrabl  19761  dprd2da  19962  ogrpaddltrbid  20059  srgbinom  20155  irredlmul  20352  rngridlmcl  21160  lidlrsppropd  21187  rngqiprngghmlem1  21230  rngqiprnglinlem2  21235  rngqiprngimf1lem  21237  rngqiprng  21239  rngqiprngimf  21240  rngqiprngghm  21242  rngqiprngimf1  21243  rngqiprngimfo  21244  rng2idl1cntr  21248  rngqiprngfulem4  21257  rngqipring1  21259  pzriprnglem6  21429  chrcl  21467  css1  21633  issubassa  21810  ply1crng  22117  ply1ring  22166  ply1lmod  22170  oftpos  22373  tposmap  22378  0opn  22825  fctop2  22926  difopn  22955  tgrest  23080  ordtbas2  23112  ordtopn3  23117  ordtcld3  23120  t1ficld  23248  resthauslem  23284  kgentopon  23459  txbasex  23487  txcnpi  23529  txdis1cn  23556  pthaus  23559  txkgen  23573  cnmptid  23582  cnmptc  23583  cnmpt1st  23589  cnmpt2nd  23590  cnmpt2c  23591  cnmptkc  23600  txconn  23610  hmeoima  23686  hmeocld  23688  xkohmeo  23736  filufint  23841  fin1aufil  23853  flftg  23917  ptcmplem2  23974  tmdmulg  24013  tmdgsum2  24017  submtmd  24025  symgtgp  24027  ghmcnp  24036  qustgpopn  24041  qustgplem  24042  ust0  24141  nrginvrcn  24613  fsumcn  24794  fsum2cn  24795  expcn  24796  expcnOLD  24798  cnheibor  24887  evth2  24892  csscld  25182  clsocv  25183  ovoliun2  25440  volfiniun  25481  dyadmbl  25534  mbfeqalem2  25576  mbfss  25580  ismbf3d  25588  mbfadd  25595  i1f0rn  25616  mbfmul  25660  itg2seq  25676  itg2monolem2  25685  itg2monolem3  25686  itg2mono  25687  itgreval  25731  itgge0  25745  itgss3  25749  iblconst  25752  itgconst  25753  ibladdlem  25754  itgfsum  25761  iblabslem  25762  itgabs  25769  cmvth  25928  lhop1lem  25951  dvfsumle  25959  dvfsumleOLD  25960  dvfsumlem2  25966  dvfsumlem2OLD  25967  ftc1lem4  25979  itgparts  25987  itgsubstlem  25988  itgsubst  25989  plydivlem1  26234  aannenlem1  26269  taylply2  26308  taylply2OLD  26309  itgulm  26350  cxpcn  26687  cxpcnOLD  26688  resqrtcn  26692  basellem1  27024  mulogsumlem  27475  mulog2sumlem2  27479  selberg2lem  27494  pntrsumo1  27509  addsuniflem  27950  ssltmul1  28092  ssltmul2  28093  precsexlem11  28161  usgrnbcnvfv  29350  ewlksfval  29587  crctcshwlkn0  29806  pjssmii  31668  rabrexfi  32493  abrexexd  32496  mptiffisupp  32681  pfxlsw2ccat  32938  cntrcrng  33057  dfufd2lem  33521  ply1degltdimlem  33642  fldgenfldext  33688  fldextrspunlem2  33697  lmatfval  33834  pl1cn  33975  esumcvg  34106  esumcvgsum  34108  sigaval  34131  sigaclfu2  34141  sigapildsys  34182  ldgenpisys  34186  measinb2  34243  braew  34262  unelcarsg  34332  carsgclctunlem2  34339  sibfof  34360  sitgclg  34362  orrvcoel  34486  orrvccel  34487  fsum2dsub  34627  fineqvpow  35145  subfaclefac  35227  cvmsss2  35325  cvmopnlem  35329  satf0suclem  35426  mpstrcl  35592  elmpps  35624  hmeoclda  36384  bj-1uplex  37059  bj-2uplex  37073  icoreclin  37408  broucube  37700  mblfinlem1  37703  cnambfre  37714  ibladdnclem  37722  iblabsnclem  37729  itgabsnc  37735  ftc1cnnclem  37737  ftc1anclem4  37742  ftc1anclem5  37743  ftc1anclem6  37744  ftc1anclem7  37745  ftc2nc  37748  areacirc  37759  zrdivrng  37999  xrnresex  38459  dalemrot  39762  dalem10  39778  arglem1N  40295  cdlemk36  41018  resopunitintvd  42125  resclunitintvd  42126  lcmineqlem2  42129  aks6d1c7lem1  42279  aks5lem2  42286  mzpconstmpt  42838  mzpresrename  42848  diophrex  42873  0dioph  42876  anrabdioph  42878  orrabdioph  42879  rabren3dioph  42913  dvradcnv2  44445  xpexb  44551  fsumcnf  45123  uzublem  45533  fprodcncf  46003  iblconstmpt  46059  itgiccshift  46083  itgperiod  46084  itgsbtaddcnst  46085  dirkercncflem2  46207  fourierdlem47  46256  saluni  46428  sge0iunmpt  46521  sge0xaddlem2  46537  sge0xadd  46538  hoidmvlelem3  46700  ctvonmbl  46792  vonct  46796  smfaddlem2  46867  smfmullem4  46897  aoprssdm  47307  rescofuf  49199  idfu1stalem  49206  idfu1sta  49207  idfu1a  49208  idfu2nda  49209  oppfuprcl  49310  lmddu  49773  cmddu  49774