Theorem eqeltrrid 2833

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

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

This theorem is referenced by:  3eltr3g  2844  dmrnssfld  5926  oprssdm  7550  offval  7642  pwexr  7721  cnvexg  7880  resfunexgALT  7906  abrexex2g  7922  opabex3d  7923  opabex3rd  7924  frxp3  8107  suppssov1  8153  suppssov2  8154  suppssfv  8158  ralxpmap  8846  unfi  9112  imafi  9240  pwfir  9242  pwfilem  9243  residfi  9265  abrexfi  9279  ssfii  9346  wdomima2g  9515  unxpwdom2  9517  tskwe  9879  ac10ct  9963  fin23lem28  10269  fin23lem30  10271  axcclem  10386  distrlem4pr  10955  iccshftr  13423  iccshftl  13425  iccdil  13427  icccntr  13429  o1res  15502  exprmfct  16650  infpnlem1  16857  4sqlem13  16904  0ram  16967  ressval3d  17192  ismred2  17540  mreexexlem2d  17586  mreexexlem4d  17588  acsfn1c  17603  acsfn2  17604  ssclem  17761  submacs  18736  symgtset  19313  symgsubmefmndALT  19317  efgrcl  19629  cntrcmnd  19756  cntrabl  19757  dprd2da  19958  ogrpaddltrbid  20055  srgbinom  20151  irredlmul  20348  rngridlmcl  21159  lidlrsppropd  21186  rngqiprngghmlem1  21229  rngqiprnglinlem2  21234  rngqiprngimf1lem  21236  rngqiprng  21238  rngqiprngimf  21239  rngqiprngghm  21241  rngqiprngimf1  21242  rngqiprngimfo  21243  rng2idl1cntr  21247  rngqiprngfulem4  21256  rngqipring1  21258  pzriprnglem6  21428  chrcl  21466  css1  21632  issubassa  21809  ply1crng  22116  ply1ring  22165  ply1lmod  22169  oftpos  22372  tposmap  22377  0opn  22824  fctop2  22925  difopn  22954  tgrest  23079  ordtbas2  23111  ordtopn3  23116  ordtcld3  23119  t1ficld  23247  resthauslem  23283  kgentopon  23458  txbasex  23486  txcnpi  23528  txdis1cn  23555  pthaus  23558  txkgen  23572  cnmptid  23581  cnmptc  23582  cnmpt1st  23588  cnmpt2nd  23589  cnmpt2c  23590  cnmptkc  23599  txconn  23609  hmeoima  23685  hmeocld  23687  xkohmeo  23735  filufint  23840  fin1aufil  23852  flftg  23916  ptcmplem2  23973  tmdmulg  24012  tmdgsum2  24016  submtmd  24024  symgtgp  24026  ghmcnp  24035  qustgpopn  24040  qustgplem  24041  ust0  24140  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  27948  ssltmul1  28090  ssltmul2  28091  precsexlem11  28159  usgrnbcnvfv  29345  ewlksfval  29582  crctcshwlkn0  29801  pjssmii  31660  rabrexfi  32485  abrexexd  32488  mptiffisupp  32666  pfxlsw2ccat  32922  cntrcrng  33053  dfufd2lem  33513  ply1degltdimlem  33611  fldgenfldext  33656  fldextrspunlem2  33665  lmatfval  33797  pl1cn  33938  esumcvg  34069  esumcvgsum  34071  sigaval  34094  sigaclfu2  34104  sigapildsys  34145  ldgenpisys  34149  measinb2  34206  braew  34225  unelcarsg  34296  carsgclctunlem2  34303  sibfof  34324  sitgclg  34326  orrvcoel  34450  orrvccel  34451  fsum2dsub  34591  fineqvpow  35079  subfaclefac  35156  cvmsss2  35254  cvmopnlem  35258  satf0suclem  35355  mpstrcl  35521  elmpps  35553  hmeoclda  36314  bj-1uplex  36989  bj-2uplex  37003  icoreclin  37338  broucube  37641  mblfinlem1  37644  cnambfre  37655  ibladdnclem  37663  iblabsnclem  37670  itgabsnc  37676  ftc1cnnclem  37678  ftc1anclem4  37683  ftc1anclem5  37684  ftc1anclem6  37685  ftc1anclem7  37686  ftc2nc  37689  areacirc  37700  zrdivrng  37940  xrnresex  38385  dalemrot  39644  dalem10  39660  arglem1N  40177  cdlemk36  40900  resopunitintvd  42007  resclunitintvd  42008  lcmineqlem2  42011  aks6d1c7lem1  42161  aks5lem2  42168  mzpconstmpt  42721  mzpresrename  42731  diophrex  42756  0dioph  42759  anrabdioph  42761  orrabdioph  42762  rabren3dioph  42796  dvradcnv2  44329  xpexb  44436  fsumcnf  45008  uzublem  45419  fprodcncf  45891  iblconstmpt  45947  itgiccshift  45971  itgperiod  45972  itgsbtaddcnst  45973  dirkercncflem2  46095  fourierdlem47  46144  saluni  46316  sge0iunmpt  46409  sge0xaddlem2  46425  sge0xadd  46426  hoidmvlelem3  46588  ctvonmbl  46680  vonct  46684  smfaddlem2  46755  smfmullem4  46785  singoutnword  46873  aoprssdm  47196  rescofuf  49075  idfu1stalem  49082  idfu1sta  49083  idfu1a  49084  idfu2nda  49085  oppfuprcl  49186  lmddu  49649  cmddu  49650