Theorem eqeltrrid 2834

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 2739	. 2 ⊢ 𝐴 = 𝐵
3		eqeltrrid.2	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
4	2, 3	eqeltrid 2833	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-clel 2804

This theorem is referenced by:  3eltr3g  2845  dmrnssfld  5940  oprssdm  7573  offval  7665  pwexr  7744  cnvexg  7903  resfunexgALT  7929  abrexexgOLD  7943  abrexex2g  7946  opabex3d  7947  opabex3rd  7948  frxp3  8133  suppssov1  8179  suppssov2  8180  suppssfv  8184  ralxpmap  8872  unfi  9141  imafi  9271  pwfir  9273  pwfilem  9274  residfi  9296  abrexfi  9310  ssfii  9377  wdomima2g  9546  unxpwdom2  9548  tskwe  9910  ac10ct  9994  fin23lem28  10300  fin23lem30  10302  axcclem  10417  distrlem4pr  10986  iccshftr  13454  iccshftl  13456  iccdil  13458  icccntr  13460  o1res  15533  exprmfct  16681  infpnlem1  16888  4sqlem13  16935  0ram  16998  ressval3d  17223  ismred2  17571  mreexexlem2d  17613  mreexexlem4d  17615  acsfn1c  17630  acsfn2  17631  ssclem  17788  submacs  18761  symgtset  19336  symgsubmefmndALT  19340  efgrcl  19652  cntrcmnd  19779  cntrabl  19780  dprd2da  19981  srgbinom  20147  irredlmul  20344  rngridlmcl  21134  lidlrsppropd  21161  rngqiprngghmlem1  21204  rngqiprnglinlem2  21209  rngqiprngimf1lem  21211  rngqiprng  21213  rngqiprngimf  21214  rngqiprngghm  21216  rngqiprngimf1  21217  rngqiprngimfo  21218  rng2idl1cntr  21222  rngqiprngfulem4  21231  rngqipring1  21233  pzriprnglem6  21403  chrcl  21441  css1  21606  issubassa  21783  ply1crng  22090  ply1ring  22139  ply1lmod  22143  oftpos  22346  tposmap  22351  0opn  22798  fctop2  22899  difopn  22928  tgrest  23053  ordtbas2  23085  ordtopn3  23090  ordtcld3  23093  t1ficld  23221  resthauslem  23257  kgentopon  23432  txbasex  23460  txcnpi  23502  txdis1cn  23529  pthaus  23532  txkgen  23546  cnmptid  23555  cnmptc  23556  cnmpt1st  23562  cnmpt2nd  23563  cnmpt2c  23564  cnmptkc  23573  txconn  23583  hmeoima  23659  hmeocld  23661  xkohmeo  23709  filufint  23814  fin1aufil  23826  flftg  23890  ptcmplem2  23947  tmdmulg  23986  tmdgsum2  23990  submtmd  23998  symgtgp  24000  ghmcnp  24009  qustgpopn  24014  qustgplem  24015  ust0  24114  nrginvrcn  24587  fsumcn  24768  fsum2cn  24769  expcn  24770  expcnOLD  24772  cnheibor  24861  evth2  24866  csscld  25156  clsocv  25157  ovoliun2  25414  volfiniun  25455  dyadmbl  25508  mbfeqalem2  25550  mbfss  25554  ismbf3d  25562  mbfadd  25569  i1f0rn  25590  mbfmul  25634  itg2seq  25650  itg2monolem2  25659  itg2monolem3  25660  itg2mono  25661  itgreval  25705  itgge0  25719  itgss3  25723  iblconst  25726  itgconst  25727  ibladdlem  25728  itgfsum  25735  iblabslem  25736  itgabs  25743  cmvth  25902  lhop1lem  25925  dvfsumle  25933  dvfsumleOLD  25934  dvfsumlem2  25940  dvfsumlem2OLD  25941  ftc1lem4  25953  itgparts  25961  itgsubstlem  25962  itgsubst  25963  plydivlem1  26208  aannenlem1  26243  taylply2  26282  taylply2OLD  26283  itgulm  26324  cxpcn  26661  cxpcnOLD  26662  resqrtcn  26666  basellem1  26998  mulogsumlem  27449  mulog2sumlem2  27453  selberg2lem  27468  pntrsumo1  27483  addsuniflem  27915  ssltmul1  28057  ssltmul2  28058  precsexlem11  28126  usgrnbcnvfv  29299  ewlksfval  29536  crctcshwlkn0  29758  pjssmii  31617  rabrexfi  32442  abrexexd  32445  mptiffisupp  32623  pfxlsw2ccat  32879  cntrcrng  33017  ogrpaddltrbid  33041  dfufd2lem  33527  ply1degltdimlem  33625  fldgenfldext  33670  fldextrspunlem2  33679  lmatfval  33811  pl1cn  33952  esumcvg  34083  esumcvgsum  34085  sigaval  34108  sigaclfu2  34118  sigapildsys  34159  ldgenpisys  34163  measinb2  34220  braew  34239  unelcarsg  34310  carsgclctunlem2  34317  sibfof  34338  sitgclg  34340  orrvcoel  34464  orrvccel  34465  fsum2dsub  34605  fineqvpow  35093  subfaclefac  35170  cvmsss2  35268  cvmopnlem  35272  satf0suclem  35369  mpstrcl  35535  elmpps  35567  hmeoclda  36328  bj-1uplex  37003  bj-2uplex  37017  icoreclin  37352  broucube  37655  mblfinlem1  37658  cnambfre  37669  ibladdnclem  37677  iblabsnclem  37684  itgabsnc  37690  ftc1cnnclem  37692  ftc1anclem4  37697  ftc1anclem5  37698  ftc1anclem6  37699  ftc1anclem7  37700  ftc2nc  37703  areacirc  37714  zrdivrng  37954  xrnresex  38399  dalemrot  39658  dalem10  39674  arglem1N  40191  cdlemk36  40914  resopunitintvd  42021  resclunitintvd  42022  lcmineqlem2  42025  aks6d1c7lem1  42175  aks5lem2  42182  mzpconstmpt  42735  mzpresrename  42745  diophrex  42770  0dioph  42773  anrabdioph  42775  orrabdioph  42776  rabren3dioph  42810  dvradcnv2  44343  xpexb  44450  fsumcnf  45022  uzublem  45433  fprodcncf  45905  iblconstmpt  45961  itgiccshift  45985  itgperiod  45986  itgsbtaddcnst  45987  dirkercncflem2  46109  fourierdlem47  46158  saluni  46330  sge0iunmpt  46423  sge0xaddlem2  46439  sge0xadd  46440  hoidmvlelem3  46602  ctvonmbl  46694  vonct  46698  smfaddlem2  46769  smfmullem4  46799  singoutnword  46887  aoprssdm  47207  rescofuf  49086  idfu1stalem  49093  idfu1sta  49094  idfu1a  49095  idfu2nda  49096  oppfuprcl  49197  lmddu  49660  cmddu  49661