Theorem eqeltrd 2114

Description: Substitution of equal classes into membership relation, deduction form. (Contributed by Raph Levien, 10-Dec-2002.)

Hypotheses

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

Assertion

Ref	Expression
eqeltrd	|- ( ph -> A e. C )

Proof of Theorem eqeltrd

Step	Hyp	Ref	Expression
1		eqeltrd.2	. 2 |- ( ph -> B e. C )
2		eqeltrd.1	. . 3 |- ( ph -> A = B )
3	2	eleq1d 2106	. 2 |- ( ph -> ( A e. C <-> B e. C ) )
4	1, 3	mpbird 156	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1243   e. wcel 1393

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033  df-clel 2036

This theorem is referenced by:  eqeltrrd  2115  3eltr4d  2121  syl5eqel  2124  syl6eqel  2128  ifcldcd  3358  intab  3644  iinexgm  3908  opexg  3964  opexgOLD  3965  tfisi  4310  imain  4981  fvmptd  5253  fvmptdf  5258  fvmptt  5262  dffo3  5314  resfunexg  5382  f1oiso2  5466  riota2df  5488  riota5f  5492  ovmpt2dxf  5626  ovmpt2df  5632  offval  5719  iunexg  5746  oprabexd  5754  fo1stresm  5788  fo2ndresm  5789  1stdm  5808  1stconst  5842  2ndconst  5843  cnvf1olem  5845  fo2ndf  5848  iunon  5899  tfrlemibacc  5940  tfrlemibfn  5942  frec0g  5983  freccl  5993  oacl  6040  omcl  6041  oeicl  6042  fidifsnen  6331  ordiso2  6357  cardcl  6361  addclpi  6425  mulclpi  6426  addclnq  6473  mulclnq  6474  addclnq0  6549  mulclnq0  6550  nqpnq0nq  6551  elnp1st2nd  6574  prarloclemcalc  6600  distrlem1prl  6680  distrlem1pru  6681  ltexprlemopl  6699  ltexprlemopu  6701  ltexprlemfl  6707  ltexprlemrl  6708  ltexprlemfu  6709  ltexprlemru  6710  addcanprlemu  6713  recexprlemloc  6729  aptiprleml  6737  caucvgprprlemopl  6795  addclsr  6838  mulclsr  6839  recexgt0sr  6858  mulextsr1lem  6864  axaddcl  6940  axaddrcl  6941  axmulcl  6942  axmulrcl  6943  axcaucvglemval  6971  subcl  7210  cru  7593  divclap  7657  redivclap  7707  cju  7913  nn1m1nn  7932  nnsub  7952  nnnn0addcl  8212  un0addcl  8215  peano2z  8281  peano2zm  8283  zaddcllemneg  8284  zaddcl  8285  nnaddm1cl  8305  nn0n0n1ge2  8311  zdivadd  8329  zdivmul  8330  zneo  8339  peano5uzti  8346  qmulz  8558  qnegcl  8571  qapne  8574  qdivcl  8577  cnref1o  8582  xnegcl  8745  xltnegi  8748  iccf1o  8872  ige3m2fz  8913  ige2m1fz1  8971  rebtwn2z  9109  flqcl  9117  ceilqcl  9150  intfracq  9162  modqcl  9168  mulqmod0  9172  modqdifz  9178  frec2uzzd  9186  frec2uzuzd  9188  frecuzrdgrrn  9194  frecuzrdgcl  9199  frecuzrdgsuc  9201  fzofig  9208  iseqovex  9219  iseqcaopr3  9240  iser0f  9251  serile  9253  expivallem  9256  exp1  9261  expcl2lemap  9267  m1expcl2  9277  expaddzap  9299  sqcl  9315  nnsqcl  9323  qsqcl  9325  zesq  9367  shftlem  9417  ovshftex  9420  shftf  9431  cjth  9446  imval  9450  recl  9453  imcl  9454  crre  9457  remim  9460  reim0b  9462  cvg1nlemcau  9583  uzin2  9586  resqrexlem1arp  9603  resqrexlemp1rp  9604  resqrexlemglsq  9620  resqrexlemga  9621  resqrtcl  9627  abscl  9649  absrpclap  9659  nn0abscl  9681  fzomaxdiflem  9708  fzomaxdif  9709  climaddc1  9849  climmulc2  9851  climsubc1  9852  climsubc2  9853  climle  9854  iisermulc2  9860  climlec2  9861  climcvg1nlem  9868  sqr2irrlem  9877  nn0seqcvgd  9880  ialgrlem1st  9881  ialgrlemconst  9882  ialgrp1  9885  qdencn  10124