Theorem eqeltrrd 2283

Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)

Hypotheses

Ref	Expression
eqeltrrd.1	|- ( ph -> A = B )
eqeltrrd.2	|- ( ph -> A e. C )

Assertion

Ref	Expression
eqeltrrd	|- ( ph -> B e. C )

Proof of Theorem eqeltrrd

Step	Hyp	Ref	Expression
1		eqeltrrd.1	. . 3 |- ( ph -> A = B )
2	1	eqcomd 2211	. 2 |- ( ph -> B = A )
3		eqeltrrd.2	. 2 |- ( ph -> A e. C )
4	2, 3	eqeltrd 2282	1 |- ( ph -> B e. C )

Syntax hints:   -> wi 4   = wceq 1373   e. wcel 2176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  3eltr3d  2288  exmid01  4243  pwntru  4244  xpexr2m  5125  funimaexg  5359  fvmptdv2  5671  ffvresb  5745  iotaexel  5906  2ndrn  6271  1st2ndbr  6272  elopabi  6283  cnvf1olem  6312  dftpos4  6351  tfrlemibxssdm  6415  tfr1onlembxssdm  6431  tfrcllembxssdm  6444  nnmordi  6604  th3qlem1  6726  infiexmid  6976  onunsnss  7016  ssfirab  7035  ssfidc  7036  fnfi  7040  fidcenumlemr  7059  elfi2  7076  ordiso2  7139  djulclb  7159  ctmlemr  7212  ctssdccl  7215  ctssdc  7217  exmidfodomrlemreseldju  7310  exmidfodomrlemr  7312  exmidapne  7374  archnqq  7532  prarloclemarch2  7534  enq0tr  7549  nqnq0  7556  addcmpblnq0  7558  mulcmpblnq0  7559  mulcanenq0ec  7560  addclnq0  7566  mulclnq0  7567  nqpnq0nq  7568  nq0m0r  7571  distrnq0  7574  addassnq0lemcl  7576  prarloclemlt  7608  prarloclem5  7615  distrlem4prl  7699  distrlem4pru  7700  ltexprlemm  7715  ltexprlemrl  7725  ltexprlemru  7727  addcanprleml  7729  cauappcvgprlemladdru  7771  prsrlem1  7857  mulgt0sr  7893  axpre-suploclemres  8016  cnegexlem2  8250  subf  8276  resubcl  8338  negcon1ad  8380  subeq0bd  8453  rimul  8660  rereim  8661  aprcl  8721  nn0nnaddcl  9328  elnn0nn  9339  zaddcllemneg  9413  zsubcl  9415  zrevaddcl  9425  elz2  9446  zdiv  9463  peano5uzti  9483  peano2uzr  9708  uzaddcl  9709  divfnzn  9744  qsubcl  9761  qrevaddcl  9767  fseq1p1m1  10218  suprzubdc  10381  modqmuladdim  10514  frec2uzrand  10552  frecuzrdglem  10558  frecuzrdg0  10560  frecuzrdgdomlem  10564  frecuzrdg0t  10569  frecuzrdgsuctlem  10570  seq3val  10607  seq3feq  10627  iseqf1olemnab  10648  seqf1oglem2  10667  seqfeq3  10676  seqfeq4g  10678  expaddzaplem  10729  expaddzap  10730  expmulzap  10732  zesq  10805  bcm1k  10907  bccl  10914  permnn  10918  seq3coll  10989  ccatrn  11068  shftuz  11161  ref  11199  imf  11200  crre  11201  rereb  11207  resqrexlemnm  11362  absf  11454  summodclem2a  11725  summodc  11727  fsumgcl  11730  fsum3  11731  fsumf1o  11734  fsumcnv  11781  mptfzshft  11786  isumlessdc  11840  geolim2  11856  prodmodclem3  11919  fprodseq  11927  fprodf1o  11932  dvdsaddre2b  12185  3dvds  12208  oexpneg  12221  nn0ob  12252  divalglemqt  12263  gcdf  12326  lcmgcdlem  12432  sqnprm  12491  sqrt2irrlem  12516  2sqpwodd  12531  fnum  12545  fden  12546  phimullem  12580  pc2dvds  12686  gzsubcl  12736  4sqlem5  12738  4sqlem9  12742  4sqlem10  12743  mul4sqlem  12749  mul4sq  12750  4sqlem11  12757  4sqlem13m  12759  4sqlem16  12762  4sqlem17  12763  4sqlem18  12764  ctiunctlemfo  12843  ptex  13129  prdsval  13138  prdsbas  13141  prdsbascl  13154  mgmsscl  13226  subsubm  13348  mhmima  13356  imasgrp2  13479  mhmmnd  13485  mulgdir  13523  subgmulg  13557  issubg2m  13558  issubgrpd2  13559  grpissubg  13563  subsubg  13566  isnsg3  13576  ssnmz  13580  eqger  13593  eqgen  13596  ecqusaddcl  13608  ghmrn  13626  ghmnsgima  13637  conjsubg  13646  conjnmz  13648  ring1  13854  reldvdsrsrg  13887  dvdsrvald  13888  dvdsrd  13889  dvdsrex  13893  0unit  13924  invrpropdg  13944  lringuplu  13991  subrngin  14008  subsubrng  14009  subrgcrng  14020  subrgin  14039  subsubrg  14040  islmodd  14088  lssvacl  14160  lssvancl1  14162  lss0cl  14164  lssvscl  14170  lssvnegcl  14171  lssincl  14180  issubrgd  14247  lidlrsppropdg  14290  2idlcpblrng  14318  zsssubrg  14380  unopn  14510  tsettps  14543  tgss2  14584  difopn  14613  resttop  14675  resttopon  14676  restco  14679  tgcn  14713  tgcnp  14714  cnptopco  14727  upxp  14777  txcn  14780  txdis  14782  cnmpt11  14788  cnmpt11f  14789  cnmpt1t  14790  cnmpt12  14792  cnmpt21  14796  cnmpt21f  14797  cnmpt2t  14798  cnmpt22  14799  cnmpt22f  14800  cnmpt1res  14801  xmeter  14941  mscl  14970  xmscl  14971  bdxmet  15006  cncfmpt1f  15103  cdivcncfap  15109  negfcncf  15111  ivthreinc  15150  cnmptlimc  15179  dvcnp2cntop  15204  elplyd  15246  plypow  15249  plyconst  15250  plyaddlem1  15252  plysub  15258  dvply2g  15271  sincn  15274  coscn  15275  relogcl  15367  mpodvdsmulf1o  15495  fsumdvdsmul  15496  mersenne  15502  perfect  15506  lgsne0  15548  lgseisenlem4  15583  lgsquadlem1  15587  pwtrufal  15971