Theorem eqeltrd 2155

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 2147	. 2 |- ( ph -> ( A e. C <-> B e. C ) )
4	1, 3	mpbird 165	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1284   e. wcel 1433

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074  df-clel 2077

This theorem is referenced by:  eqeltrrd  2156  3eltr4d  2162  syl5eqel  2165  syl6eqel  2169  ifcldadc  3378  ifcldcd  3381  intab  3665  iinexgm  3929  opexg  3983  tfisi  4328  imain  5001  fvmptd  5274  fvmptdf  5279  fvmptt  5283  dffo3  5335  resfunexg  5403  f1oiso2  5486  riota2df  5508  riota5f  5512  ovmpt2dxf  5646  ovmpt2df  5652  offval  5739  iunexg  5766  oprabexd  5774  fo1stresm  5808  fo2ndresm  5809  1stdm  5828  1stconst  5862  2ndconst  5863  cnvf1olem  5865  fo2ndf  5868  f1od2  5876  iunon  5922  tfrlemibacc  5963  tfrlemibfn  5965  frec0g  6006  freccl  6016  oacl  6063  omcl  6064  oeicl  6065  fidifsnen  6355  en2eqpr  6380  fnfi  6388  relcnvfi  6391  supclti  6411  supubti  6412  suplubti  6413  supelti  6415  ordiso2  6446  cardcl  6450  addclpi  6517  mulclpi  6518  addclnq  6565  mulclnq  6566  addclnq0  6641  mulclnq0  6642  nqpnq0nq  6643  elnp1st2nd  6666  prarloclemcalc  6692  distrlem1prl  6772  distrlem1pru  6773  ltexprlemopl  6791  ltexprlemopu  6793  ltexprlemfl  6799  ltexprlemrl  6800  ltexprlemfu  6801  ltexprlemru  6802  addcanprlemu  6805  recexprlemloc  6821  aptiprleml  6829  caucvgprprlemopl  6887  addclsr  6930  mulclsr  6931  recexgt0sr  6950  mulextsr1lem  6956  axaddcl  7032  axaddrcl  7033  axmulcl  7034  axmulrcl  7035  axcaucvglemval  7063  subcl  7307  cru  7702  divclap  7766  redivclap  7819  lbinfcl  8027  cju  8038  nn1m1nn  8057  nnsub  8077  nnnn0addcl  8318  un0addcl  8321  peano2z  8387  peano2zm  8389  zaddcllemneg  8390  zaddcl  8391  nnaddm1cl  8412  nn0n0n1ge2  8418  zdivadd  8436  zdivmul  8437  suprzclex  8445  zneo  8448  peano5uzti  8455  supinfneg  8683  infsupneg  8684  qmulz  8708  qnegcl  8721  qapne  8724  qdivcl  8728  cnref1o  8733  xnegcl  8899  xltnegi  8902  iccf1o  9026  ige3m2fz  9068  ige2m1fz1  9126  rebtwn2z  9263  flqcl  9277  ceilqcl  9310  intfracq  9322  modqcl  9328  mulqmod0  9332  modqdifz  9338  zmodcl  9346  modfzo0difsn  9397  modsumfzodifsn  9398  frec2uzzd  9402  frec2uzuzd  9404  frecuzrdgrrn  9410  frecuzrdgcl  9415  frecuzrdgsuc  9417  fzofig  9424  iseqovex  9439  iseqcaopr3  9460  iser0f  9472  serile  9474  expivallem  9477  exp1  9482  expcl2lemap  9488  m1expcl2  9498  expaddzap  9520  sqcl  9537  nnsqcl  9545  qsqcl  9547  zesq  9591  facp1  9657  faccl  9662  facdiv  9665  bcval  9676  bcrpcl  9680  bcp1n  9688  bcpasc  9693  permnn  9698  shftlem  9704  ovshftex  9707  shftf  9718  cjth  9733  imval  9737  recl  9740  imcl  9741  crre  9744  remim  9747  reim0b  9749  cvg1nlemcau  9870  uzin2  9873  resqrexlem1arp  9891  resqrexlemp1rp  9892  resqrexlemglsq  9908  resqrexlemga  9909  resqrtcl  9915  abscl  9937  absrpclap  9947  nn0abscl  9971  fzomaxdiflem  9998  fzomaxdif  9999  maxabslemab  10092  maxcl  10096  minmax  10112  climaddc1  10167  climmulc2  10169  climsubc1  10170  climsubc2  10171  climle  10172  iisermulc2  10178  climlec2  10179  climcvg1nlem  10186  dvdsval2  10198  sqoddm1div8z  10286  zssinfcl  10344  infssuzex  10345  infssuzcldc  10347  gcdval  10351  gcdn0cl  10354  gcddvds  10355  divgcdnnr  10367  nn0seqcvgd  10423  ialgrlem1st  10424  ialgrlemconst  10425  ialgrp1  10428  eucalgf  10437  eucalglt  10439  lcmval  10445  lcmcllem  10449  lcmgcdlem  10459  cncongr2  10486  sqrt2irrlem  10540  oddpwdclemxy  10547  oddpwdclemdc  10551  qdencn  10785