Theorem eleqtrd 2266

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

Syntax hints:   -> wi 4   = wceq 1363   e. wcel 2158

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 1457  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-4 1520  ax-17 1536  ax-ial 1544  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-cleq 2180  df-clel 2183

This theorem is referenced by:  eleqtrrd  2267  3eltr3d  2270  eleqtrid  2276  eleqtrdi  2280  opth1  4248  0nelop  4260  tfisi  4598  nnpredlt  4635  iotam  5220  ercl  6560  erth  6593  ecelqsdm  6619  phpm  6879  exmidpweq  6923  cc2lem  7279  cc3  7281  suplocexprlemmu  7731  suplocexprlemloc  7734  lincmb01cmp  10017  fzopth  10075  fzoaddel2  10207  fzosubel2  10209  fzocatel  10213  zpnn0elfzo1  10222  fzoend  10236  peano2fzor  10246  monoord2  10491  ser3mono  10492  bcpasc  10760  zfz1isolemiso  10833  fisum0diag2  11469  isumsplit  11513  prodmodclem3  11597  prodmodclem2a  11598  nnmindc  12049  nnminle  12050  basmexd  12536  mgm1  12808  grpidd  12821  sgrppropd  12838  ismndd  12860  mndpropd  12863  issubmnd  12865  grpidd2  12938  imasgrp  13006  subginvcl  13075  subgcl  13076  subgsub  13078  subgmulg  13080  1nsgtrivd  13111  rngass  13191  rngcl  13196  rngpropd  13207  imasrng  13208  srgcl  13222  srgass  13223  srg1zr  13239  srgpcomp  13242  srgpcompp  13243  srgpcomppsc  13244  crngcom  13266  ringass  13268  ringidmlem  13274  ringidss  13281  ringpropd  13290  imasring  13312  qusring2  13314  mulgass3  13333  dvdsrd  13342  1unit  13355  unitmulcl  13361  dvrvald  13382  rdivmuldivd  13392  lringuplu  13416  subrngmcl  13429  subrg1  13451  subrgmcl  13453  subrgdv  13458  subrgunit  13459  aprval  13471  aprirr  13472  aprsym  13473  aprcotr  13474  lmodprop2d  13537  lidlss  13665  lidl0cl  13672  lidlacl  13673  lidlnegcl  13674  rnglidlmsgrp  13686  2idllidld  13694  2idlridld  13695  2idlcpblrng  13711  qus1  13714  quscrng  13720  iscnp4  14014  cnrest2r  14033  txbasval  14063  txlm  14075  xmetunirn  14154  xblss2ps  14200  blbas  14229  mopntopon  14239  isxms2  14248  metcnpi  14311  metcnpi2  14312  tgioo  14342  cncfmpt2fcntop  14381  limccl  14424  limcimolemlt  14429  limccnp2cntop  14442  dvmulxxbr  14462  dvcoapbr  14467  dvcjbr  14468  dvrecap  14473