Theorem eleqtrd 2256

Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)

Hypotheses

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

Assertion

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

Proof of Theorem eleqtrd

Step	Hyp	Ref	Expression
1		eleqtrd.1	. 2 |- ( ph -> A e. B )
2		eleqtrd.2	. . 3 |- ( ph -> B = C )
3	2	eleq2d 2247	. 2 |- ( ph -> ( A e. B <-> A e. C ) )
4	1, 3	mpbid 147	1 |- ( ph -> A e. C )

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

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  eleqtrrd  2257  3eltr3d  2260  eleqtrid  2266  eleqtrdi  2270  opth1  4237  0nelop  4249  tfisi  4587  nnpredlt  4624  iotam  5209  ercl  6546  erth  6579  ecelqsdm  6605  phpm  6865  exmidpweq  6909  cc2lem  7265  cc3  7267  suplocexprlemmu  7717  suplocexprlemloc  7720  lincmb01cmp  10003  fzopth  10061  fzoaddel2  10193  fzosubel2  10195  fzocatel  10199  zpnn0elfzo1  10208  fzoend  10222  peano2fzor  10232  monoord2  10477  ser3mono  10478  bcpasc  10746  zfz1isolemiso  10819  fisum0diag2  11455  isumsplit  11499  prodmodclem3  11583  prodmodclem2a  11584  nnmindc  12035  nnminle  12036  basmexd  12522  mgm1  12789  grpidd  12802  ismndd  12838  mndpropd  12841  issubmnd  12843  grpidd2  12914  subginvcl  13043  subgcl  13044  subgsub  13046  subgmulg  13048  1nsgtrivd  13079  srgcl  13153  srgass  13154  srg1zr  13170  srgpcomp  13173  srgpcompp  13174  srgpcomppsc  13175  crngcom  13197  ringass  13199  ringidmlem  13205  ringidss  13212  ringpropd  13217  mulgass3  13254  dvdsrd  13263  1unit  13276  unitmulcl  13282  dvrvald  13303  rdivmuldivd  13313  lringuplu  13337  subrg1  13352  subrgmcl  13354  subrgdv  13359  subrgunit  13360  aprval  13372  aprirr  13373  aprsym  13374  aprcotr  13375  lmodprop2d  13438  iscnp4  13721  cnrest2r  13740  txbasval  13770  txlm  13782  xmetunirn  13861  xblss2ps  13907  blbas  13936  mopntopon  13946  isxms2  13955  metcnpi  14018  metcnpi2  14019  tgioo  14049  cncfmpt2fcntop  14088  limccl  14131  limcimolemlt  14136  limccnp2cntop  14149  dvmulxxbr  14169  dvcoapbr  14174  dvcjbr  14175  dvrecap  14180