Theorem eqeltrrid 2874

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 2778	. 2 ⊢ 𝐴 = 𝐵
3		eqeltrrid.2	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
4	2, 3	eqeltrid 2873	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:  3eltr3g  2885  dmrnssfld  5965  oprssdm  7592  offval  7684  pwexr  7764  cnvexg  7921  resfunexgALT  7945  abrexex2g  7961  opabex3d  7962  opabex3rd  7963  frxp3  8147  suppssov1  8193  suppssov2  8194  suppssfv  8198  ralxpmap  8894  unfi  9155  imafi  9275  pwfir  9276  pwfilem  9277  resfnfinfin  9294  residfi  9295  abrexfi  9309  ssfii  9379  wdomima2g  9548  unxpwdom2  9550  tskwe  9936  ac10ct  10018  fin23lem28  10324  fin23lem30  10326  axcclem  10441  distrlem4pr  11011  iccshftr  13513  iccshftl  13515  iccdil  13517  icccntr  13519  o1res  15611  exprmfct  16763  infpnlem1  16970  4sqlem13  17017  0ram  17080  ressval3d  17306  ismred2  17655  mreexexlem2d  17701  mreexexlem4d  17703  acsfn1c  17718  acsfn2  17719  ssclem  17876  submacs  18886  symgtset  19469  symgsubmefmndALT  19473  efgrcl  19785  cntrcmnd  19912  cntrabl  19913  dprd2da  20114  ogrpaddltrbid  20211  srgbinom  20313  irredlmul  20510  rngridlmcl  21320  lidlrsppropd  21352  rngqiprngghmlem1  21398  rngqiprnglinlem2  21403  rngqiprngimf1lem  21405  rngqiprng  21407  rngqiprngimf  21408  rngqiprngghm  21410  rngqiprngimf1  21411  rngqiprngimfo  21412  rng2idl1cntr  21416  rngqiprngfulem4  21425  rngqipring1  21427  pzriprnglem6  21605  chrcl  21643  css1  21809  issubassa  21986  ply1crng  22327  ply1ring  22376  ply1lmod  22380  oftpos  22578  tposmap  22583  0opn  23030  fctop2  23131  difopn  23160  tgrest  23285  ordtbas2  23317  ordtopn3  23322  ordtcld3  23325  t1ficld  23453  resthauslem  23489  kgentopon  23664  txbasex  23692  txcnpi  23734  txdis1cn  23761  pthaus  23764  txkgen  23778  cnmptid  23787  cnmptc  23788  cnmpt1st  23794  cnmpt2nd  23795  cnmpt2c  23796  cnmptkc  23805  txconn  23815  hmeoima  23891  hmeocld  23893  xkohmeo  23941  filufint  24046  fin1aufil  24058  flftg  24122  ptcmplem2  24179  tmdmulg  24218  tmdgsum2  24222  submtmd  24230  symgtgp  24232  ghmcnp  24241  qustgpopn  24246  qustgplem  24247  ust0  24346  nrginvrcn  24818  fsumcn  24998  fsum2cn  24999  expcn  25000  cnheibor  25083  evth2  25088  csscld  25377  clsocv  25378  ovoliun2  25634  volfiniun  25675  dyadmbl  25728  mbfeqalem2  25770  mbfss  25774  ismbf3d  25782  mbfadd  25789  i1f0rn  25810  mbfmul  25854  itg2seq  25870  itg2monolem2  25879  itg2monolem3  25880  itg2mono  25881  itgreval  25925  itgge0  25939  itgss3  25943  iblconst  25946  itgconst  25947  ibladdlem  25948  itgfsum  25955  iblabslem  25956  itgabs  25963  cmvth  26119  lhop1lem  26141  dvfsumle  26149  dvfsumlem2  26155  ftc1lem4  26167  itgparts  26175  itgsubstlem  26176  itgsubst  26177  plydivlem1  26423  aannenlem1  26458  taylply2  26497  itgulm  26537  cxpcn  26876  resqrtcn  26880  basellem1  27211  mulogsumlem  27661  mulog2sumlem2  27665  selberg2lem  27680  pntrsumo1  27695  addsuniflem  28160  sltmuls1  28306  sltmuls2  28307  precsexlem11  28376  usgrnbcnvfv  29656  ewlksfval  29892  crctcshwlkn0  30111  pjssmii  31974  rabrexfi  32793  abrexexd  32796  mptiffisupp  32979  pfxlsw2ccat  33211  gsummulsubdishift2s  33332  cntrcrng  33342  dfufd2lem  33784  selvply1rhmlemb  33854  vietalem  33914  ply1degltdimlem  33957  fldgenfldext  34003  fldextrspunlem2  34012  lmatfval  34149  pl1cn  34290  esumcvg  34421  esumcvgsum  34423  sigaval  34446  sigaclfu2  34456  sigapildsys  34497  ldgenpisys  34501  measinb2  34558  braew  34577  unelcarsg  34647  carsgclctunlem2  34654  sibfof  34675  sitgclg  34677  orrvcoel  34801  orrvccel  34802  fsum2dsub  34939  fineqvpow  35461  subfaclefac  35601  cvmsss2  35699  cvmopnlem  35703  satf0suclem  35800  mpstrcl  35966  elmpps  35998  hmeoclda  36767  bj-1uplex  37566  bj-2uplex  37580  icoreclin  37925  broucube  38227  mblfinlem1  38230  cnambfre  38241  ibladdnclem  38249  iblabsnclem  38256  itgabsnc  38262  ftc1cnnclem  38264  ftc1anclem4  38269  ftc1anclem5  38270  ftc1anclem6  38271  ftc1anclem7  38272  ftc2nc  38275  areacirc  38286  zrdivrng  38526  xrnresex  39002  dalemrot  40355  dalem10  40371  arglem1N  40888  cdlemk36  41611  resopunitintvd  42717  resclunitintvd  42718  lcmineqlem2  42721  aks6d1c7lem1  42871  aks5lem2  42878  mzpconstmpt  43397  mzpresrename  43407  diophrex  43432  0dioph  43435  anrabdioph  43437  orrabdioph  43438  rabren3dioph  43468  dvradcnv2  44983  xpexb  45088  fsumcnf  45667  uzublem  46070  fprodcncf  46540  iblconstmpt  46596  itgiccshift  46620  itgperiod  46621  itgsbtaddcnst  46622  dirkercncflem2  46744  fourierdlem47  46793  saluni  46965  sge0iunmpt  47058  sge0xaddlem2  47074  sge0xadd  47075  hoicvr  47188  hoidmvlelem3  47237  ctvonmbl  47329  vonct  47333  smfaddlem2  47404  smfmullem4  47434  aoprssdm  47862  rescofuf  49790  idfu1stalem  49797  idfu1sta  49798  idfu1a  49799  idfu2nda  49800  oppfuprcl  49901  lmddu  50364  cmddu  50365