Theorem eleqtrd 2317

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   e. wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  eleqtrrd  2318  3eltr3d  2321  eleqtrid  2327  eleqtrdi  2331  opth1  4376  0nelop  4388  tfisi  4734  nnpredlt  4771  iotam  5369  ercl  6818  erth  6853  ecelqsdm  6879  phpm  7167  exmidpweq  7216  pw1if  7584  cc2lem  7632  cc3  7634  suplocexprlemmu  8085  suplocexprlemloc  8088  lincmb01cmp  10415  fzopth  10477  fzoaddel2  10618  fzosubel2  10623  fzocatel  10627  zpnn0elfzo1  10636  fzoend  10650  peano2fzor  10660  infssfzcldc  10679  infssfzledc  10680  monoord2  10936  ser3mono  10937  bcpasc  11218  zfz1isolemiso  11305  swrdclg  11436  fisum0diag2  12230  isumsplit  12274  prodmodclem3  12358  prodmodclem2a  12359  nnmindc  12827  nnminle  12828  bassetsnn  13458  basmexd  13462  basm  13463  slotm  13464  mgm1  13739  grpidd  13752  gzsumress  13761  sgrppropd  13777  ismndd  13799  mndpropd  13802  issubmnd  13804  imasmnd  13809  grpidd2  13895  imasgrp  13963  submmulg  14018  subginvcl  14035  subgcl  14036  subgsub  14038  subgmulg  14040  1nsgtrivd  14071  quseccl0g  14083  kerf1ghm  14126  prdsbasfn  14230  prdsbasprj  14231  pwsplusgval  14257  pwsmulrval  14258  pwsinvg  14264  rngass  14287  rngcl  14292  rngpropd  14303  imasrng  14304  srgcl  14323  srgass  14324  srgpcomp  14343  srgpcompp  14344  srgpcomppsc  14345  crngcom  14367  ringass  14369  ringidmlem  14376  ringidss  14383  ringpropd  14392  imasring  14418  qusring2  14420  mulgass3  14440  dvdsrd  14450  1unit  14463  unitmulcl  14469  dvrvald  14490  rdivmuldivd  14500  elrhmunit  14533  rhmunitinv  14534  lringuplu  14552  subrngmcl  14566  subrg1  14588  subrgmcl  14590  subrgdv  14595  subrgunit  14596  resrhm  14605  aprval  14640  aprirr  14644  aprsym  14645  aprcotr  14646  opprdrng  14669  lmodprop2d  14734  lidlss  14862  lidl0cl  14869  lidlacl  14870  lidlnegcl  14871  rnglidlmsgrp  14883  2idllidld  14892  2idlridld  14893  2idlcpblrng  14909  qus1  14912  quscrng  14919  rspsn  14920  znf1o  15035  assapropd  15063  psrbagfi  15108  psrelbas  15115  iscnp4  15368  cnrest2r  15387  txbasval  15417  txlm  15429  xmetunirn  15508  xblss2ps  15554  blbas  15583  mopntopon  15593  isxms2  15602  metcnpi  15665  metcnpi2  15666  tgioo  15704  cncfmpt2fcntop  15749  limccl  15809  limcimolemlt  15814  limccnp2cntop  15827  dvmulxxbr  15852  dvcoapbr  15857  dvcjbr  15858  dvrecap  15863  plyaddlem1  15897  plymullem1  15898  plycoeid3  15907  ppinprm  16171  lgseisenlem4  16290  usgr1vr  16587  clwwlkccatlem  16739