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  4236  0nelop  4248  tfisi  4586  nnpredlt  4623  iotam  5208  ercl  6545  erth  6578  ecelqsdm  6604  phpm  6864  exmidpweq  6908  cc2lem  7264  cc3  7266  suplocexprlemmu  7716  suplocexprlemloc  7719  lincmb01cmp  10002  fzopth  10060  fzoaddel2  10192  fzosubel2  10194  fzocatel  10198  zpnn0elfzo1  10207  fzoend  10221  peano2fzor  10231  monoord2  10476  ser3mono  10477  bcpasc  10745  zfz1isolemiso  10818  fisum0diag2  11454  isumsplit  11498  prodmodclem3  11582  prodmodclem2a  11583  nnmindc  12034  nnminle  12035  basmexd  12521  mgm1  12788  grpidd  12801  ismndd  12837  mndpropd  12840  issubmnd  12842  grpidd2  12913  subginvcl  13041  subgcl  13042  subgsub  13044  subgmulg  13046  1nsgtrivd  13077  srgcl  13151  srgass  13152  srg1zr  13168  srgpcomp  13171  srgpcompp  13172  srgpcomppsc  13173  crngcom  13195  ringass  13197  ringidmlem  13203  ringidss  13210  ringpropd  13215  mulgass3  13252  dvdsrd  13261  1unit  13274  unitmulcl  13280  dvrvald  13301  rdivmuldivd  13311  lringuplu  13335  subrg1  13350  subrgmcl  13352  subrgdv  13357  subrgunit  13358  aprval  13370  aprirr  13371  aprsym  13372  aprcotr  13373  iscnp4  13688  cnrest2r  13707  txbasval  13737  txlm  13749  xmetunirn  13828  xblss2ps  13874  blbas  13903  mopntopon  13913  isxms2  13922  metcnpi  13985  metcnpi2  13986  tgioo  14016  cncfmpt2fcntop  14055  limccl  14098  limcimolemlt  14103  limccnp2cntop  14116  dvmulxxbr  14136  dvcoapbr  14141  dvcjbr  14142  dvrecap  14147