Theorem eqeltrrd 2166

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 2094	. 2 |- ( ph -> B = A )
3		eqeltrrd.2	. 2 |- ( ph -> A e. C )
4	2, 3	eqeltrd 2165	1 |- ( ph -> B e. C )

Syntax hints:   -> wi 4   = wceq 1290   e. wcel 1439

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-4 1446  ax-17 1465  ax-ial 1473  ax-ext 2071

This theorem depends on definitions:  df-bi 116  df-cleq 2082  df-clel 2085

This theorem is referenced by:  3eltr3d  2171  exmid01  4040  xpexr2m  4887  funimaexg  5113  fvmptdv2  5407  ffvresb  5477  2ndrn  5969  1st2ndbr  5970  elopabi  5981  cnvf1olem  6005  dftpos4  6044  tfrlemibxssdm  6108  tfr1onlembxssdm  6124  tfrcllembxssdm  6137  nnmordi  6291  th3qlem1  6410  infiexmid  6649  onunsnss  6683  ssfirab  6699  ssfidc  6700  fnfi  6702  fidcenumlemr  6720  ordiso2  6784  djulclb  6803  ctmlemr  6846  exmidfodomrlemreseldju  6889  exmidfodomrlemr  6891  archnqq  7039  prarloclemarch2  7041  enq0tr  7056  nqnq0  7063  addcmpblnq0  7065  mulcmpblnq0  7066  mulcanenq0ec  7067  addclnq0  7073  mulclnq0  7074  nqpnq0nq  7075  nq0m0r  7078  distrnq0  7081  addassnq0lemcl  7083  prarloclemlt  7115  prarloclem5  7122  distrlem4prl  7206  distrlem4pru  7207  ltexprlemm  7222  ltexprlemrl  7232  ltexprlemru  7234  addcanprleml  7236  cauappcvgprlemladdru  7278  prsrlem1  7351  mulgt0sr  7386  cnegexlem2  7721  subf  7747  resubcl  7809  negcon1ad  7851  subeq0bd  7920  rimul  8125  rereim  8126  nn0nnaddcl  8767  elnn0nn  8778  zaddcllemneg  8852  zsubcl  8854  zrevaddcl  8863  elz2  8881  zdiv  8897  peano5uzti  8917  peano2uzr  9136  uzaddcl  9137  divfnzn  9169  qsubcl  9186  qrevaddcl  9192  fseq1p1m1  9571  modqmuladdim  9837  frec2uzrand  9875  frecuzrdglem  9881  frecuzrdg0  9883  frecuzrdgdomlem  9887  frecuzrdg0t  9892  frecuzrdgsuctlem  9893  iseqvalt  9936  seq3val  9937  iseqfeq  9959  seq3feq  9960  iseqf1olemnab  9980  iseqdistr  10008  expaddzaplem  10061  expaddzap  10062  expmulzap  10064  zesq  10135  bcm1k  10231  bccl  10238  permnn  10242  iseqcoll  10310  shftuz  10314  ref  10352  imf  10353  crre  10354  rereb  10360  resqrexlemnm  10514  absf  10606  isummolem2a  10834  isummo  10836  fsumgcl  10840  fisum  10841  fsumf1o  10845  fsumcnv  10894  mptfzshft  10899  isumlessdc  10953  geolim2  10969  oexpneg  11218  nn0ob  11249  divalglemqt  11260  gcdf  11305  lcmgcdlem  11400  sqnprm  11458  sqrt2irrlem  11481  2sqpwodd  11495  fnum  11509  fden  11510  phimullem  11542  unopn  11767  tsettps  11799  tgss2  11842  difopn  11871