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  4038  xpexr2m  4885  funimaexg  5111  fvmptdv2  5405  ffvresb  5475  2ndrn  5967  1st2ndbr  5968  elopabi  5979  cnvf1olem  6003  dftpos4  6042  tfrlemibxssdm  6106  tfr1onlembxssdm  6122  tfrcllembxssdm  6135  nnmordi  6289  th3qlem1  6408  infiexmid  6647  onunsnss  6681  ssfirab  6697  ssfidc  6698  fnfi  6700  fidcenumlemr  6718  ordiso2  6782  djulclb  6801  exmidfodomrlemreseldju  6880  exmidfodomrlemr  6882  archnqq  7030  prarloclemarch2  7032  enq0tr  7047  nqnq0  7054  addcmpblnq0  7056  mulcmpblnq0  7057  mulcanenq0ec  7058  addclnq0  7064  mulclnq0  7065  nqpnq0nq  7066  nq0m0r  7069  distrnq0  7072  addassnq0lemcl  7074  prarloclemlt  7106  prarloclem5  7113  distrlem4prl  7197  distrlem4pru  7198  ltexprlemm  7213  ltexprlemrl  7223  ltexprlemru  7225  addcanprleml  7227  cauappcvgprlemladdru  7269  prsrlem1  7342  mulgt0sr  7377  cnegexlem2  7712  subf  7738  resubcl  7800  negcon1ad  7842  subeq0bd  7911  rimul  8116  rereim  8117  nn0nnaddcl  8758  elnn0nn  8769  zaddcllemneg  8843  zsubcl  8845  zrevaddcl  8854  elz2  8872  zdiv  8888  peano5uzti  8908  peano2uzr  9127  uzaddcl  9128  divfnzn  9160  qsubcl  9177  qrevaddcl  9183  fseq1p1m1  9562  modqmuladdim  9828  frec2uzrand  9866  frecuzrdglem  9872  frecuzrdg0  9874  frecuzrdgdomlem  9878  frecuzrdg0t  9883  frecuzrdgsuctlem  9884  iseqvalt  9927  seq3val  9928  iseqfeq  9950  seq3feq  9951  iseqf1olemnab  9971  iseqdistr  9999  expaddzaplem  10052  expaddzap  10053  expmulzap  10055  zesq  10126  bcm1k  10222  bccl  10229  permnn  10233  iseqcoll  10301  shftuz  10305  ref  10343  imf  10344  crre  10345  rereb  10351  resqrexlemnm  10505  absf  10597  isummolem2a  10825  isummo  10827  fsumgcl  10831  fisum  10832  fsumf1o  10836  fsumcnv  10885  mptfzshft  10890  isumlessdc  10944  geolim2  10960  oexpneg  11209  nn0ob  11240  divalglemqt  11251  gcdf  11296  lcmgcdlem  11391  sqnprm  11449  sqrt2irrlem  11472  2sqpwodd  11486  fnum  11500  fden  11501  phimullem  11533  unopn  11758  tsettps  11790  tgss2  11833  difopn  11862