Theorem eleqtrd 2310

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 2301	. 2 |- ( ph -> ( A e. B <-> A e. C ) )
4	1, 3	mpbid 147	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1397   e. wcel 2202

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  eleqtrrd  2311  3eltr3d  2314  eleqtrid  2320  eleqtrdi  2324  opth1  4328  0nelop  4340  tfisi  4685  nnpredlt  4722  iotam  5318  ercl  6713  erth  6748  ecelqsdm  6774  phpm  7052  exmidpweq  7101  pw1if  7443  cc2lem  7485  cc3  7487  suplocexprlemmu  7938  suplocexprlemloc  7941  lincmb01cmp  10238  fzopth  10296  fzoaddel2  10436  fzosubel2  10441  fzocatel  10445  zpnn0elfzo1  10454  fzoend  10468  peano2fzor  10478  monoord2  10749  ser3mono  10750  bcpasc  11029  zfz1isolemiso  11104  swrdclg  11235  fisum0diag2  12026  isumsplit  12070  prodmodclem3  12154  prodmodclem2a  12155  nnmindc  12623  nnminle  12624  bassetsnn  13157  basmexd  13161  basm  13162  prdsbasfn  13382  prdsbasprj  13383  pwsplusgval  13396  pwsmulrval  13397  mgm1  13471  grpidd  13484  gsumress  13496  sgrppropd  13514  ismndd  13538  mndpropd  13541  issubmnd  13543  imasmnd  13554  grpidd2  13642  pwsinvg  13713  imasgrp  13716  submmulg  13771  subginvcl  13788  subgcl  13789  subgsub  13791  subgmulg  13793  1nsgtrivd  13824  quseccl0g  13836  kerf1ghm  13879  rngass  13971  rngcl  13976  rngpropd  13987  imasrng  13988  srgcl  14002  srgass  14003  srg1zr  14019  srgpcomp  14022  srgpcompp  14023  srgpcomppsc  14024  crngcom  14046  ringass  14048  ringidmlem  14054  ringidss  14061  ringpropd  14070  imasring  14096  qusring2  14098  mulgass3  14117  dvdsrd  14127  1unit  14140  unitmulcl  14146  dvrvald  14167  rdivmuldivd  14177  elrhmunit  14210  rhmunitinv  14211  lringuplu  14229  subrngmcl  14242  subrg1  14264  subrgmcl  14266  subrgdv  14271  subrgunit  14272  resrhm  14281  aprval  14315  aprirr  14316  aprsym  14317  aprcotr  14318  lmodprop2d  14381  lidlss  14509  lidl0cl  14516  lidlacl  14517  lidlnegcl  14518  rnglidlmsgrp  14530  2idllidld  14539  2idlridld  14540  2idlcpblrng  14556  qus1  14559  quscrng  14566  rspsn  14567  znf1o  14684  psrbagfi  14706  psrelbas  14708  iscnp4  14961  cnrest2r  14980  txbasval  15010  txlm  15022  xmetunirn  15101  xblss2ps  15147  blbas  15176  mopntopon  15186  isxms2  15195  metcnpi  15258  metcnpi2  15259  tgioo  15297  cncfmpt2fcntop  15342  limccl  15402  limcimolemlt  15407  limccnp2cntop  15420  dvmulxxbr  15445  dvcoapbr  15450  dvcjbr  15451  dvrecap  15456  plyaddlem1  15490  plymullem1  15491  plycoeid3  15500  lgseisenlem4  15821  usgr1vr  16118  clwwlkccatlem  16270