Theorem eqeltrrd 2253

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

Syntax hints:   -> wi 4   = wceq 1353   e. wcel 2146

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 1445  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-4 1508  ax-17 1524  ax-ial 1532  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-cleq 2168  df-clel 2171

This theorem is referenced by:  3eltr3d  2258  exmid01  4193  pwntru  4194  xpexr2m  5062  funimaexg  5292  fvmptdv2  5597  ffvresb  5671  2ndrn  6174  1st2ndbr  6175  elopabi  6186  cnvf1olem  6215  dftpos4  6254  tfrlemibxssdm  6318  tfr1onlembxssdm  6334  tfrcllembxssdm  6347  nnmordi  6507  th3qlem1  6627  infiexmid  6867  onunsnss  6906  ssfirab  6923  ssfidc  6924  fnfi  6926  fidcenumlemr  6944  elfi2  6961  ordiso2  7024  djulclb  7044  ctmlemr  7097  ctssdccl  7100  ctssdc  7102  exmidfodomrlemreseldju  7189  exmidfodomrlemr  7191  archnqq  7391  prarloclemarch2  7393  enq0tr  7408  nqnq0  7415  addcmpblnq0  7417  mulcmpblnq0  7418  mulcanenq0ec  7419  addclnq0  7425  mulclnq0  7426  nqpnq0nq  7427  nq0m0r  7430  distrnq0  7433  addassnq0lemcl  7435  prarloclemlt  7467  prarloclem5  7474  distrlem4prl  7558  distrlem4pru  7559  ltexprlemm  7574  ltexprlemrl  7584  ltexprlemru  7586  addcanprleml  7588  cauappcvgprlemladdru  7630  prsrlem1  7716  mulgt0sr  7752  axpre-suploclemres  7875  cnegexlem2  8107  subf  8133  resubcl  8195  negcon1ad  8237  subeq0bd  8310  rimul  8516  rereim  8517  aprcl  8577  nn0nnaddcl  9180  elnn0nn  9191  zaddcllemneg  9265  zsubcl  9267  zrevaddcl  9276  elz2  9297  zdiv  9314  peano5uzti  9334  peano2uzr  9558  uzaddcl  9559  divfnzn  9594  qsubcl  9611  qrevaddcl  9617  fseq1p1m1  10064  modqmuladdim  10337  frec2uzrand  10375  frecuzrdglem  10381  frecuzrdg0  10383  frecuzrdgdomlem  10387  frecuzrdg0t  10392  frecuzrdgsuctlem  10393  seq3val  10428  seq3feq  10442  iseqf1olemnab  10458  seqfeq3  10482  expaddzaplem  10533  expaddzap  10534  expmulzap  10536  zesq  10608  bcm1k  10708  bccl  10715  permnn  10719  seq3coll  10790  shftuz  10794  ref  10832  imf  10833  crre  10834  rereb  10840  resqrexlemnm  10995  absf  11087  summodclem2a  11357  summodc  11359  fsumgcl  11362  fsum3  11363  fsumf1o  11366  fsumcnv  11413  mptfzshft  11418  isumlessdc  11472  geolim2  11488  prodmodclem3  11551  fprodseq  11559  fprodf1o  11564  oexpneg  11849  nn0ob  11880  divalglemqt  11891  suprzubdc  11920  gcdf  11940  lcmgcdlem  12044  sqnprm  12103  sqrt2irrlem  12128  2sqpwodd  12143  fnum  12157  fden  12158  phimullem  12192  pc2dvds  12296  gzsubcl  12345  4sqlem5  12347  4sqlem9  12351  4sqlem10  12352  mul4sqlem  12358  mul4sq  12359  ctiunctlemfo  12407  mgmsscl  12646  mhmima  12737  mhmmnd  12841  mulgdir  12875  ring1  13032  unopn  13074  tsettps  13107  tgss2  13150  difopn  13179  resttop  13241  resttopon  13242  restco  13245  tgcn  13279  tgcnp  13280  cnptopco  13293  upxp  13343  txcn  13346  txdis  13348  cnmpt11  13354  cnmpt11f  13355  cnmpt1t  13356  cnmpt12  13358  cnmpt21  13362  cnmpt21f  13363  cnmpt2t  13364  cnmpt22  13365  cnmpt22f  13366  cnmpt1res  13367  xmeter  13507  mscl  13536  xmscl  13537  bdxmet  13572  cncfmpt1f  13655  cdivcncfap  13658  negfcncf  13660  cnmptlimc  13714  dvcnp2cntop  13734  sincn  13761  coscn  13762  relogcl  13854  lgsne0  14010  pwtrufal  14307