Theorem eqeltrd 2308

Description: Substitution of equal classes into membership relation, deduction form. (Contributed by Raph Levien, 10-Dec-2002.)

Hypotheses

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

Assertion

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

Proof of Theorem eqeltrd

Step	Hyp	Ref	Expression
1		eqeltrd.2	. 2 |- ( ph -> B e. C )
2		eqeltrd.1	. . 3 |- ( ph -> A = B )
3	2	eleq1d 2300	. 2 |- ( ph -> ( A e. C <-> B e. C ) )
4	1, 3	mpbird 167	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1398   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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2213

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

This theorem is referenced by:  eqeltrrd  2309  3eltr4d  2315  eqeltrid  2318  eqeltrdi  2322  ifcldadc  3639  ifcldcd  3647  intab  3962  disjiun  4088  iinexgm  4249  opexg  4326  tfisi  4691  nnpredcl  4727  opabssxpd  4768  imain  5419  fvmptd  5736  fvmptdf  5743  fvmptt  5747  elfvmptrab  5751  dffo3  5802  resfunexg  5883  f1oiso2  5978  riota2df  6003  riota5f  6008  ovmpodxf  6157  ovmpodf  6163  offval  6252  ofvalg  6254  offeq  6258  iunexg  6290  oprabexd  6298  fo1stresm  6333  fo2ndresm  6334  oprssdmm  6343  1stdm  6354  1stconst  6395  2ndconst  6396  cnvf1olem  6398  fo2ndf  6401  f1od2  6409  iunon  6493  tfrlemibacc  6535  tfrlemibfn  6537  tfr1onlembacc  6551  tfr1onlembfn  6553  tfrcllembacc  6564  tfrcllembfn  6566  tfrcl  6573  rdgon  6595  frec0g  6606  freccllem  6611  frecfcllem  6613  frecsuclem  6615  oacl  6671  omcl  6672  oeicl  6673  nntr2  6714  mptelixpg  6946  fidifsnen  7100  en2eqpr  7142  unfiin  7161  tpfidceq  7165  ssfirab  7172  fnfi  7178  relcnvfi  7183  fidcenumlemr  7197  snopfsuppdc  7224  fsuppcorn  7226  elfi2  7231  supclti  7257  supubti  7258  suplubti  7259  supelti  7261  ordiso2  7294  djulclr  7308  djurclr  7309  djulcl  7310  djurcl  7311  djuss  7329  updjudhcoinlf  7339  updjudhcoinrg  7340  ctssdclemn0  7369  ctssdccl  7370  ctssdc  7372  enumctlemm  7373  nninfwlpoimlemg  7434  cardcl  7445  exmidontriimlem2  7497  exmidapne  7539  cc2lem  7545  cc3  7547  addclpi  7607  mulclpi  7608  addclnq  7655  mulclnq  7656  addclnq0  7731  mulclnq0  7732  nqpnq0nq  7733  elnp1st2nd  7756  prarloclemcalc  7782  distrlem1prl  7862  distrlem1pru  7863  ltexprlemopl  7881  ltexprlemopu  7883  ltexprlemfl  7889  ltexprlemrl  7890  ltexprlemfu  7891  ltexprlemru  7892  addcanprlemu  7895  recexprlemloc  7911  aptiprleml  7919  caucvgprprlemopl  7977  suplocexprlemex  8002  addclsr  8033  mulclsr  8034  recexgt0sr  8053  mulextsr1lem  8060  suplocsrlemb  8086  suplocsrlempr  8087  suplocsrlem  8088  axaddcl  8144  axaddrcl  8145  axmulcl  8146  axmulrcl  8147  axcaucvglemval  8177  subcl  8437  cru  8841  aprcl  8885  aptap  8889  divclap  8917  redivclap  8970  diveqap1bd  9075  lbinfcl  9188  cju  9200  nn1m1nn  9220  nnsub  9241  nnnn0addcl  9491  un0addcl  9494  peano2z  9576  peano2zm  9578  zaddcllemneg  9579  zaddcl  9580  nnaddm1cl  9602  nn0n0n1ge2  9611  zdivadd  9630  zdivmul  9631  suprzclex  9639  zneo  9642  peano5uzti  9649  supinfneg  9890  infsupneg  9891  qmulz  9918  qnegcl  9931  qapne  9934  qdivcl  9938  cnref1o  9946  xnegcl  10128  xltnegi  10131  xaddnemnf  10153  xaddnepnf  10154  xnegdi  10164  xnpcan  10168  xltadd1  10172  xposdif  10178  xleaddadd  10183  iccf1o  10301  ige3m2fz  10346  ige2m1fz1  10406  zssinfcl  10555  infssuzex  10556  infssuzcldc  10558  zsupssdc  10561  suprzcl2dc  10562  rebtwn2z  10577  flqcl  10596  flapcl  10598  ceilqcl  10633  intfracq  10645  modqcl  10651  mulqmod0  10655  modqdifz  10661  zmodcl  10669  modfzo0difsn  10720  modsumfzodifsn  10721  frec2uzzd  10725  frec2uzsucd  10726  frec2uzuzd  10727  frecuzrdgrrn  10733  frec2uzrdg  10734  frecuzrdgrcl  10735  frecuzrdgsuc  10739  frecuzrdgrclt  10740  frecuzrdgg  10741  frecuzrdgsuctlem  10748  fzofig  10757  iseqovex  10783  seq3val  10785  seqvalcd  10786  seqf  10789  seqovcd  10792  seq3clss  10796  seq3caopr3  10816  iseqf1olemnab  10826  iseqf1olemqk  10832  iseqf1olemjpcl  10833  iseqf1olemqpcl  10834  iseqf1olemfvp  10835  seq3f1olemqsumkj  10836  seq3f1olemqsum  10838  seq3f1oleml  10841  seq3f1o  10842  seqf1oglem2a  10843  seqf1oglem1  10844  seqf1oglem2  10845  seq3distr  10857  ser0f  10859  ser3le  10862  exp3vallem  10865  exp3val  10866  exp1  10870  expcl2lemap  10876  m1expcl2  10886  expaddzap  10908  sqcl  10925  nnsqcl  10934  qsqcl  10936  zesq  10983  facp1  11055  faccl  11060  facdiv  11063  bcval  11074  bcrpcl  11078  bcp1n  11086  bcpasc  11091  permnn  11096  hashennn  11105  hashcl  11106  lencl  11183  wrdexg  11190  elovmpowrd  11221  lswcl  11230  ccatcl  11236  ccatrn  11252  lswccatn0lsw  11254  ccatalpha  11256  s1cl  11264  swrdclg  11297  swrdwrdsymbg  11311  ccatswrd  11317  pfxval  11321  fnpfx  11324  pfxclg  11325  pfxwrdsymbg  11337  ccatpfx  11348  lenrevpfxcctswrd  11359  wrdind  11369  wrd2ind  11370  shftlem  11456  ovshftex  11459  shftf  11470  seq3shft  11478  cjth  11486  imval  11490  recl  11493  imcl  11494  crre  11497  remim  11500  reim0b  11502  cvg1nlemcau  11624  uzin2  11627  resqrexlem1arp  11645  resqrexlemp1rp  11646  resqrexlemglsq  11662  resqrexlemga  11663  resqrtcl  11669  abscl  11691  absrpclap  11701  nn0abscl  11725  fzomaxdiflem  11752  fzomaxdif  11753  maxabslemab  11846  maxcl  11850  zmaxcl  11864  minmax  11870  mincl  11871  xrmaxcl  11892  xrmaxaddlem  11900  xrminmax  11905  xrmincl  11906  xrmineqinf  11909  xrminrpcl  11914  reccn2ap  11953  climaddc1  11969  climmulc2  11971  climsubc1  11972  climsubc2  11973  climle  11974  climlec2  11981  climcvg1nlem  11989  sumrbdclem  12018  fsum3cvg  12019  summodclem3  12021  summodclem2a  12022  zsumdc  12025  fsumgcl  12027  fsum3  12028  isumss  12032  fisumss  12033  isumss2  12034  fsum3cvg2  12035  fsum3ser  12038  fsumcl2lem  12039  fsumcllem  12040  fsumadd  12047  sumsnf  12050  fsumsplitsn  12051  isumcl  12066  isummulc2  12067  isumrecl  12070  isumge0  12071  isumadd  12072  fsum2dlemstep  12075  fisumcom2  12079  mptfzshft  12083  fsumrev  12084  fsummulc2  12089  iserabs  12116  isumshft  12131  isumsplit  12132  isum1p  12133  isumrpcl  12135  isumle  12136  isumlessdc  12137  trireciplem  12141  expcnvap0  12143  expcnvre  12144  expcnv  12145  explecnv  12146  geolim  12152  geolim2  12153  geo2lim  12157  cvgratnnlemsumlt  12169  cvgratz  12173  mertenslemub  12175  mertenslemi1  12176  mertenslem2  12177  mertensabs  12178  prodf1f  12184  prodfdivap  12188  prodrbdclem  12212  fproddccvg  12213  prodmodclem3  12216  prodmodclem2a  12217  zproddc  12220  fprodseq  12224  fprodntrivap  12225  prodssdc  12230  fprodmul  12232  prodsnf  12233  fprodsplitdc  12237  fprodunsn  12245  fprodcl2lem  12246  fprodcllem  12247  fprodabs  12257  fprodrev  12260  fprod2dlemstep  12263  fprodcom2fi  12267  fprodsplitsn  12274  efcllemp  12299  ef0lem  12301  efcvgfsum  12308  reefcl  12309  ege2le3  12312  efcj  12314  efaddlem  12315  eftlcvg  12328  eftlcl  12329  reeftlcl  12330  eftlub  12331  efsep  12332  effsumlt  12333  efgt1p2  12336  efgt1p  12337  reeff1  12341  tanclap  12350  resincl  12361  recoscl  12362  retanclap  12363  eirraplem  12418  dvdsval2  12431  fsumdvds  12483  sqoddm1div8z  12527  bitsinv1lem  12602  gcdval  12610  gcdn0cl  12613  gcddvds  12614  divgcdnnr  12627  uzwodc  12688  nn0seqcvgd  12693  ialgrlem1st  12694  ialgrlemconst  12695  algrf  12697  algrp1  12698  eucalgf  12707  eucalglt  12709  lcmval  12715  lcmcllem  12719  lcmgcdlem  12729  cncongr2  12756  sqrt2irrlem  12813  oddpwdclemxy  12821  oddpwdclemdc  12825  qden1elz  12857  phicl2  12866  phimullem  12877  eulerthlemth  12884  prmdiv  12887  odzcllem  12895  pythagtriplem8  12925  pythagtriplem9  12926  pcval  12949  pczcl  12951  pcqcl  12959  dvdsprmpweqle  12990  pcaddlem  12992  pcmptcl  12995  pcmpt  12996  pockthlem  13009  pockthg  13010  zgz  13026  gznegcl  13028  gzcjcl  13029  gzaddcl  13030  gzmulcl  13031  gzabssqcl  13034  4sqlem5  13035  4sqlem4a  13044  mul4sqlem  13046  mul4sq  13047  4sqlemafi  13048  4sqlemffi  13049  4sqleminfi  13050  4sqexercise1  13051  4sqlem16  13059  4sqlem17  13060  ennnfonelemjn  13103  ennnfonelemg  13104  ennnfonelemp1  13107  ctinfomlemom  13128  ctiunctlemfo  13140  nninfdclemcl  13149  nninfdclemf  13150  nninfdclemp1  13151  setsex  13194  strsetsid  13195  strslfv3  13208  bassetsnn  13219  ressex  13228  ressbas2d  13231  strressid  13234  tgvalex  13426  ptex  13427  prdsex  13432  prdsval  13436  imasex  13468  imasival  13469  imasbas  13470  imasplusg  13471  imasmulr  13472  imasaddfn  13480  imasaddval  13481  imasaddf  13482  imasmulfn  13483  imasmulval  13484  imasmulf  13485  qusval  13486  qusex  13488  qusaddvallemg  13496  qusaddflemg  13497  qusaddval  13498  qusaddf  13499  qusmulval  13500  qusmulf  13501  mgm1  13533  gsumress  13558  gsumprval  13562  prdsplusgsgrpcl  13577  prdsplusgcl  13609  prdsidlem  13610  pwsmnd  13613  mhmex  13625  subsubm  13646  0subm  13647  mhmeql  13655  gsumwsubmcl  13659  gsumfzcl  13662  grpsubval  13709  grplinv  13713  pwsgrp  13774  qusgrp2  13780  mulgval  13789  mulgex  13790  mulgfng  13791  mulg1  13796  mulgnnp1  13797  mulgnnsubcl  13801  mulgnn0subcl  13802  mulgsubcl  13803  mulgnndir  13818  subgex  13843  subgsubcl  13852  issubgrpd  13858  subsubg  13864  nsgconj  13873  0nsg  13881  triv1nsgd  13885  eqgex  13888  eqger  13891  eqgcpbl  13895  ghmex  13922  ghmpreima  13933  ghmnsgpreima  13936  conjnmz  13946  gsumfzsubmcl  14005  gsumsplit0  14013  mgpex  14019  rngmgpf  14031  qusrng  14052  mgpf  14105  qusring2  14160  opprex  14167  opprrng  14171  opprring  14173  dvdsrex  14193  opprunitd  14205  dvrvald  14229  dvrcl  14230  unitdvcl  14231  invrpropdg  14244  subsubrng  14309  subrgcrng  14320  subrgsubm  14329  subrgugrp  14335  subsubrg  14340  rnrhmsubrg  14347  aprcotr  14381  rmodislmod  14447  lssvsubcl  14462  islss3  14475  lspex  14491  ellspsn  14513  sraex  14542  rlmlmod  14560  lidlex  14569  rspex  14570  lidl0cl  14579  lidlacl  14580  lidlnegcl  14581  ridl0  14606  ridl1  14607  2idlelbas  14612  cnsubglem  14675  expghmap  14703  mulgrhm  14705  zrhex  14717  znbaslemnn  14735  psrval  14762  psrbagfi  14770  psrbagcon  14772  psrbasg  14775  mplsubgfilemm  14799  mplsubgfilemcl  14800  mplsubgfileminv  14801  mplgrpfi  14807  iunopn  14813  toponmax  14836  tgtop  14879  tgiun  14884  tgidm  14885  ntropn  14928  tgrest  14980  restopnb  14992  cnovex  15007  cnclima  15034  txvalex  15065  txtop  15071  tx1cn  15080  tx2cn  15081  txcnp  15082  txcnmpt  15084  txdis1cn  15089  cnmptcom  15109  imasnopn  15110  hmeocnv  15118  hmeores  15126  txhmeo  15130  txswaphmeo  15132  ispsmet  15134  xmetres  15193  metres  15194  blex  15198  xmeter  15247  xmetresbl  15251  mopntopon  15254  isxms2  15263  xmetxp  15318  xmettx  15321  txmetcnp  15329  qtopbasss  15332  qtopbas  15333  reopnap  15357  ioo2blex  15363  blssioo  15364  tgioo  15365  fsumcncntop  15378  expcn  15380  cncfval  15383  divccncfap  15401  cdivcncfap  15415  divcncfap  15425  maxcncf  15426  mincncf  15427  ivthdec  15455  hoverb  15459  limccnpcntop  15486  dvrecap  15524  elplyd  15552  ply1termlem  15553  ply1term  15554  plymullem1  15559  plyaddlem  15560  plymullem  15561  plycolemc  15569  plyco  15570  plycj  15572  plycn  15573  plyreres  15575  dvply1  15576  dvply2g  15577  pilem3  15594  tanrpcl  15648  cosordlem  15660  ioocosf1o  15665  rpcncxpcl  15713  rpcxpcl  15714  rpabscxpbnd  15751  rplogbcl  15757  pellexlem1  15791  sgmnncl  15802  mpodvdsmulf1o  15804  fsumdvdsmul  15805  mersenne  15811  perfectlem2  15814  lgslem1  15819  lgsval  15823  lgscllem  15826  lgsne0  15857  gausslemma2dlem4  15883  lgseisenlem1  15889  lgsquadlem1  15896  lgsquadlem2  15897  2sqlem3  15936  2sqlem8  15942  vtxex  15959  iedgex  15960  edgvalg  16000  edgopval  16003  edgstruct  16005  usgrausgrien  16110  ausgrumgrien  16111  ausgrusgrien  16112  uspgr1ewopdc  16185  usgr2v1e2w  16187  uhgrspansubgrlem  16217  vtxdgfif  16234  vtxdfifiun  16238  1loopgrvd2fi  16246  1loopgrvd0fi  16247  1hevtxdg0fi  16248  1hevtxdg1en  16249  p1evtxdeqfilem  16252  vdegp1bid  16256  wlkex  16266  wlkelvv  16290  clwwlkccat  16342  clwwlknonex2lem1  16378  clwwlknonex2lem2  16379  clwwlknonex2  16380  trlsegvdeglem6  16406  trlsegvdeglem7  16407  trlsegvdegfi  16408  eupth2lem3lem1fi  16409  eupth2lem3lem2fi  16410  eupth2lem3lem5  16413  eupth2lembfi  16418  eulerpathprum  16421  depindlem1  16447  depindlem2  16448  djucllem  16518  012of  16713  2o01f  16714  nninfsellemeq  16740  qdencn  16755  cvgcmp2nlemabs  16764  trilpolemclim  16768  trilpolemisumle  16770  trilpolemeq1  16772  trilpolemlt1  16773  nconstwlpolemgt0  16797  gfsumval  16809  gfsumsn  16814  gfsumcl  16816