Theorem eqeltrrd 2243

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

Syntax hints:   -> wi 4   = wceq 1343   e. wcel 2136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161

This theorem is referenced by:  3eltr3d  2248  exmid01  4176  pwntru  4177  xpexr2m  5044  funimaexg  5271  fvmptdv2  5574  ffvresb  5647  2ndrn  6148  1st2ndbr  6149  elopabi  6160  cnvf1olem  6188  dftpos4  6227  tfrlemibxssdm  6291  tfr1onlembxssdm  6307  tfrcllembxssdm  6320  nnmordi  6480  th3qlem1  6599  infiexmid  6839  onunsnss  6878  ssfirab  6895  ssfidc  6896  fnfi  6898  fidcenumlemr  6916  elfi2  6933  ordiso2  6996  djulclb  7016  ctmlemr  7069  ctssdccl  7072  ctssdc  7074  exmidfodomrlemreseldju  7152  exmidfodomrlemr  7154  archnqq  7354  prarloclemarch2  7356  enq0tr  7371  nqnq0  7378  addcmpblnq0  7380  mulcmpblnq0  7381  mulcanenq0ec  7382  addclnq0  7388  mulclnq0  7389  nqpnq0nq  7390  nq0m0r  7393  distrnq0  7396  addassnq0lemcl  7398  prarloclemlt  7430  prarloclem5  7437  distrlem4prl  7521  distrlem4pru  7522  ltexprlemm  7537  ltexprlemrl  7547  ltexprlemru  7549  addcanprleml  7551  cauappcvgprlemladdru  7593  prsrlem1  7679  mulgt0sr  7715  axpre-suploclemres  7838  cnegexlem2  8070  subf  8096  resubcl  8158  negcon1ad  8200  subeq0bd  8273  rimul  8479  rereim  8480  aprcl  8540  nn0nnaddcl  9141  elnn0nn  9152  zaddcllemneg  9226  zsubcl  9228  zrevaddcl  9237  elz2  9258  zdiv  9275  peano5uzti  9295  peano2uzr  9519  uzaddcl  9520  divfnzn  9555  qsubcl  9572  qrevaddcl  9578  fseq1p1m1  10025  modqmuladdim  10298  frec2uzrand  10336  frecuzrdglem  10342  frecuzrdg0  10344  frecuzrdgdomlem  10348  frecuzrdg0t  10353  frecuzrdgsuctlem  10354  seq3val  10389  seq3feq  10403  iseqf1olemnab  10419  seqfeq3  10443  expaddzaplem  10494  expaddzap  10495  expmulzap  10497  zesq  10569  bcm1k  10669  bccl  10676  permnn  10680  seq3coll  10751  shftuz  10755  ref  10793  imf  10794  crre  10795  rereb  10801  resqrexlemnm  10956  absf  11048  summodclem2a  11318  summodc  11320  fsumgcl  11323  fsum3  11324  fsumf1o  11327  fsumcnv  11374  mptfzshft  11379  isumlessdc  11433  geolim2  11449  prodmodclem3  11512  fprodseq  11520  fprodf1o  11525  oexpneg  11810  nn0ob  11841  divalglemqt  11852  suprzubdc  11881  gcdf  11901  lcmgcdlem  12005  sqnprm  12064  sqrt2irrlem  12089  2sqpwodd  12104  fnum  12118  fden  12119  phimullem  12153  pc2dvds  12257  gzsubcl  12306  4sqlem5  12308  4sqlem9  12312  4sqlem10  12313  mul4sqlem  12319  mul4sq  12320  ctiunctlemfo  12368  unopn  12603  tsettps  12636  tgss2  12679  difopn  12708  resttop  12770  resttopon  12771  restco  12774  tgcn  12808  tgcnp  12809  cnptopco  12822  upxp  12872  txcn  12875  txdis  12877  cnmpt11  12883  cnmpt11f  12884  cnmpt1t  12885  cnmpt12  12887  cnmpt21  12891  cnmpt21f  12892  cnmpt2t  12893  cnmpt22  12894  cnmpt22f  12895  cnmpt1res  12896  xmeter  13036  mscl  13065  xmscl  13066  bdxmet  13101  cncfmpt1f  13184  cdivcncfap  13187  negfcncf  13189  cnmptlimc  13243  dvcnp2cntop  13263  sincn  13290  coscn  13291  relogcl  13383  lgsne0  13539  pwtrufal  13837