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 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:  eqeltrrd  2309  3eltr4d  2315  eqeltrid  2318  eqeltrdi  2322  ifcldadc  3635  ifcldcd  3643  intab  3957  disjiun  4083  iinexgm  4244  opexg  4320  tfisi  4685  nnpredcl  4721  opabssxpd  4762  imain  5412  fvmptd  5727  fvmptdf  5734  fvmptt  5738  elfvmptrab  5742  dffo3  5794  resfunexg  5875  f1oiso2  5968  riota2df  5993  riota5f  5998  ovmpodxf  6147  ovmpodf  6153  offval  6243  ofvalg  6245  offeq  6249  iunexg  6281  oprabexd  6289  fo1stresm  6324  fo2ndresm  6325  oprssdmm  6334  1stdm  6345  1stconst  6386  2ndconst  6387  cnvf1olem  6389  fo2ndf  6392  f1od2  6400  iunon  6450  tfrlemibacc  6492  tfrlemibfn  6494  tfr1onlembacc  6508  tfr1onlembfn  6510  tfrcllembacc  6521  tfrcllembfn  6523  tfrcl  6530  rdgon  6552  frec0g  6563  freccllem  6568  frecfcllem  6570  frecsuclem  6572  oacl  6628  omcl  6629  oeicl  6630  nntr2  6671  mptelixpg  6903  fidifsnen  7057  en2eqpr  7099  unfiin  7118  tpfidceq  7122  ssfirab  7129  fnfi  7135  relcnvfi  7140  fidcenumlemr  7154  elfi2  7171  supclti  7197  supubti  7198  suplubti  7199  supelti  7201  ordiso2  7234  djulclr  7248  djurclr  7249  djulcl  7250  djurcl  7251  djuss  7269  updjudhcoinlf  7279  updjudhcoinrg  7280  ctssdclemn0  7309  ctssdccl  7310  ctssdc  7312  enumctlemm  7313  nninfwlpoimlemg  7374  cardcl  7385  exmidontriimlem2  7437  exmidapne  7479  cc2lem  7485  cc3  7487  addclpi  7547  mulclpi  7548  addclnq  7595  mulclnq  7596  addclnq0  7671  mulclnq0  7672  nqpnq0nq  7673  elnp1st2nd  7696  prarloclemcalc  7722  distrlem1prl  7802  distrlem1pru  7803  ltexprlemopl  7821  ltexprlemopu  7823  ltexprlemfl  7829  ltexprlemrl  7830  ltexprlemfu  7831  ltexprlemru  7832  addcanprlemu  7835  recexprlemloc  7851  aptiprleml  7859  caucvgprprlemopl  7917  suplocexprlemex  7942  addclsr  7973  mulclsr  7974  recexgt0sr  7993  mulextsr1lem  8000  suplocsrlemb  8026  suplocsrlempr  8027  suplocsrlem  8028  axaddcl  8084  axaddrcl  8085  axmulcl  8086  axmulrcl  8087  axcaucvglemval  8117  subcl  8378  cru  8782  aprcl  8826  aptap  8830  divclap  8858  redivclap  8911  diveqap1bd  9016  lbinfcl  9129  cju  9141  nn1m1nn  9161  nnsub  9182  nnnn0addcl  9432  un0addcl  9435  peano2z  9515  peano2zm  9517  zaddcllemneg  9518  zaddcl  9519  nnaddm1cl  9541  nn0n0n1ge2  9550  zdivadd  9569  zdivmul  9570  suprzclex  9578  zneo  9581  peano5uzti  9588  supinfneg  9829  infsupneg  9830  qmulz  9857  qnegcl  9870  qapne  9873  qdivcl  9877  cnref1o  9885  xnegcl  10067  xltnegi  10070  xaddnemnf  10092  xaddnepnf  10093  xnegdi  10103  xnpcan  10107  xltadd1  10111  xposdif  10117  xleaddadd  10122  iccf1o  10239  ige3m2fz  10284  ige2m1fz1  10344  zssinfcl  10493  infssuzex  10494  infssuzcldc  10496  zsupssdc  10499  suprzcl2dc  10500  rebtwn2z  10515  flqcl  10534  flapcl  10536  ceilqcl  10571  intfracq  10583  modqcl  10589  mulqmod0  10593  modqdifz  10599  zmodcl  10607  modfzo0difsn  10658  modsumfzodifsn  10659  frec2uzzd  10663  frec2uzsucd  10664  frec2uzuzd  10665  frecuzrdgrrn  10671  frec2uzrdg  10672  frecuzrdgrcl  10673  frecuzrdgsuc  10677  frecuzrdgrclt  10678  frecuzrdgg  10679  frecuzrdgsuctlem  10686  fzofig  10695  iseqovex  10721  seq3val  10723  seqvalcd  10724  seqf  10727  seqovcd  10730  seq3clss  10734  seq3caopr3  10754  iseqf1olemnab  10764  iseqf1olemqk  10770  iseqf1olemjpcl  10771  iseqf1olemqpcl  10772  iseqf1olemfvp  10773  seq3f1olemqsumkj  10774  seq3f1olemqsum  10776  seq3f1oleml  10779  seq3f1o  10780  seqf1oglem2a  10781  seqf1oglem1  10782  seqf1oglem2  10783  seq3distr  10795  ser0f  10797  ser3le  10800  exp3vallem  10803  exp3val  10804  exp1  10808  expcl2lemap  10814  m1expcl2  10824  expaddzap  10846  sqcl  10863  nnsqcl  10872  qsqcl  10874  zesq  10921  facp1  10993  faccl  10998  facdiv  11001  bcval  11012  bcrpcl  11016  bcp1n  11024  bcpasc  11029  permnn  11034  hashennn  11043  hashcl  11044  lencl  11118  wrdexg  11125  elovmpowrd  11156  lswcl  11165  ccatcl  11171  ccatrn  11187  lswccatn0lsw  11189  ccatalpha  11191  s1cl  11199  swrdclg  11232  swrdwrdsymbg  11246  ccatswrd  11252  pfxval  11256  fnpfx  11259  pfxclg  11260  pfxwrdsymbg  11272  ccatpfx  11283  lenrevpfxcctswrd  11294  wrdind  11304  wrd2ind  11305  shftlem  11378  ovshftex  11381  shftf  11392  seq3shft  11400  cjth  11408  imval  11412  recl  11415  imcl  11416  crre  11419  remim  11422  reim0b  11424  cvg1nlemcau  11546  uzin2  11549  resqrexlem1arp  11567  resqrexlemp1rp  11568  resqrexlemglsq  11584  resqrexlemga  11585  resqrtcl  11591  abscl  11613  absrpclap  11623  nn0abscl  11647  fzomaxdiflem  11674  fzomaxdif  11675  maxabslemab  11768  maxcl  11772  zmaxcl  11786  minmax  11792  mincl  11793  xrmaxcl  11814  xrmaxaddlem  11822  xrminmax  11827  xrmincl  11828  xrmineqinf  11831  xrminrpcl  11836  reccn2ap  11875  climaddc1  11891  climmulc2  11893  climsubc1  11894  climsubc2  11895  climle  11896  climlec2  11903  climcvg1nlem  11911  sumrbdclem  11940  fsum3cvg  11941  summodclem3  11943  summodclem2a  11944  zsumdc  11947  fsumgcl  11949  fsum3  11950  isumss  11954  fisumss  11955  isumss2  11956  fsum3cvg2  11957  fsum3ser  11960  fsumcl2lem  11961  fsumcllem  11962  fsumadd  11969  sumsnf  11972  fsumsplitsn  11973  isumcl  11988  isummulc2  11989  isumrecl  11992  isumge0  11993  isumadd  11994  fsum2dlemstep  11997  fisumcom2  12001  mptfzshft  12005  fsumrev  12006  fsummulc2  12011  iserabs  12038  isumshft  12053  isumsplit  12054  isum1p  12055  isumrpcl  12057  isumle  12058  isumlessdc  12059  trireciplem  12063  expcnvap0  12065  expcnvre  12066  expcnv  12067  explecnv  12068  geolim  12074  geolim2  12075  geo2lim  12079  cvgratnnlemsumlt  12091  cvgratz  12095  mertenslemub  12097  mertenslemi1  12098  mertenslem2  12099  mertensabs  12100  prodf1f  12106  prodfdivap  12110  prodrbdclem  12134  fproddccvg  12135  prodmodclem3  12138  prodmodclem2a  12139  zproddc  12142  fprodseq  12146  fprodntrivap  12147  prodssdc  12152  fprodmul  12154  prodsnf  12155  fprodsplitdc  12159  fprodunsn  12167  fprodcl2lem  12168  fprodcllem  12169  fprodabs  12179  fprodrev  12182  fprod2dlemstep  12185  fprodcom2fi  12189  fprodsplitsn  12196  efcllemp  12221  ef0lem  12223  efcvgfsum  12230  reefcl  12231  ege2le3  12234  efcj  12236  efaddlem  12237  eftlcvg  12250  eftlcl  12251  reeftlcl  12252  eftlub  12253  efsep  12254  effsumlt  12255  efgt1p2  12258  efgt1p  12259  reeff1  12263  tanclap  12272  resincl  12283  recoscl  12284  retanclap  12285  eirraplem  12340  dvdsval2  12353  fsumdvds  12405  sqoddm1div8z  12449  bitsinv1lem  12524  gcdval  12532  gcdn0cl  12535  gcddvds  12536  divgcdnnr  12549  uzwodc  12610  nn0seqcvgd  12615  ialgrlem1st  12616  ialgrlemconst  12617  algrf  12619  algrp1  12620  eucalgf  12629  eucalglt  12631  lcmval  12637  lcmcllem  12641  lcmgcdlem  12651  cncongr2  12678  sqrt2irrlem  12735  oddpwdclemxy  12743  oddpwdclemdc  12747  qden1elz  12779  phicl2  12788  phimullem  12799  eulerthlemth  12806  prmdiv  12809  odzcllem  12817  pythagtriplem8  12847  pythagtriplem9  12848  pcval  12871  pczcl  12873  pcqcl  12881  dvdsprmpweqle  12912  pcaddlem  12914  pcmptcl  12917  pcmpt  12918  pockthlem  12931  pockthg  12932  zgz  12948  gznegcl  12950  gzcjcl  12951  gzaddcl  12952  gzmulcl  12953  gzabssqcl  12956  4sqlem5  12957  4sqlem4a  12966  mul4sqlem  12968  mul4sq  12969  4sqlemafi  12970  4sqlemffi  12971  4sqleminfi  12972  4sqexercise1  12973  4sqlem16  12981  4sqlem17  12982  ennnfonelemjn  13025  ennnfonelemg  13026  ennnfonelemp1  13029  ctinfomlemom  13050  ctiunctlemfo  13062  nninfdclemcl  13071  nninfdclemf  13072  nninfdclemp1  13073  setsex  13116  strsetsid  13117  strslfv3  13130  bassetsnn  13141  ressex  13150  ressbas2d  13153  strressid  13156  tgvalex  13348  ptex  13349  prdsex  13354  prdsval  13358  imasex  13390  imasival  13391  imasbas  13392  imasplusg  13393  imasmulr  13394  imasaddfn  13402  imasaddval  13403  imasaddf  13404  imasmulfn  13405  imasmulval  13406  imasmulf  13407  qusval  13408  qusex  13410  qusaddvallemg  13418  qusaddflemg  13419  qusaddval  13420  qusaddf  13421  qusmulval  13422  qusmulf  13423  mgm1  13455  gsumress  13480  gsumprval  13484  prdsplusgsgrpcl  13499  prdsplusgcl  13531  prdsidlem  13532  pwsmnd  13535  mhmex  13547  subsubm  13568  0subm  13569  mhmeql  13577  gsumwsubmcl  13581  gsumfzcl  13584  grpsubval  13631  grplinv  13635  pwsgrp  13696  qusgrp2  13702  mulgval  13711  mulgex  13712  mulgfng  13713  mulg1  13718  mulgnnp1  13719  mulgnnsubcl  13723  mulgnn0subcl  13724  mulgsubcl  13725  mulgnndir  13740  subgex  13765  subgsubcl  13774  issubgrpd  13780  subsubg  13786  nsgconj  13795  0nsg  13803  triv1nsgd  13807  eqgex  13810  eqger  13813  eqgcpbl  13817  ghmex  13844  ghmpreima  13855  ghmnsgpreima  13858  conjnmz  13868  gsumfzsubmcl  13927  gsumsplit0  13935  mgpex  13941  rngmgpf  13953  qusrng  13974  mgpf  14027  qusring2  14082  opprex  14089  opprrng  14093  opprring  14095  dvdsrex  14115  opprunitd  14127  dvrvald  14151  dvrcl  14152  unitdvcl  14153  invrpropdg  14166  subsubrng  14231  subrgcrng  14242  subrgsubm  14251  subrgugrp  14257  subsubrg  14262  rnrhmsubrg  14269  aprcotr  14302  rmodislmod  14368  lssvsubcl  14383  islss3  14396  lspex  14412  ellspsn  14434  sraex  14463  rlmlmod  14481  lidlex  14490  rspex  14491  lidl0cl  14500  lidlacl  14501  lidlnegcl  14502  ridl0  14527  ridl1  14528  2idlelbas  14533  cnsubglem  14596  expghmap  14624  mulgrhm  14626  zrhex  14638  znbaslemnn  14656  psrval  14683  psrbagfi  14690  psrbasg  14691  mplsubgfilemm  14715  mplsubgfilemcl  14716  mplsubgfileminv  14717  mplgrpfi  14723  iunopn  14729  toponmax  14752  tgtop  14795  tgiun  14800  tgidm  14801  ntropn  14844  tgrest  14896  restopnb  14908  cnovex  14923  cnclima  14950  txvalex  14981  txtop  14987  tx1cn  14996  tx2cn  14997  txcnp  14998  txcnmpt  15000  txdis1cn  15005  cnmptcom  15025  imasnopn  15026  hmeocnv  15034  hmeores  15042  txhmeo  15046  txswaphmeo  15048  ispsmet  15050  xmetres  15109  metres  15110  blex  15114  xmeter  15163  xmetresbl  15167  mopntopon  15170  isxms2  15179  xmetxp  15234  xmettx  15237  txmetcnp  15245  qtopbasss  15248  qtopbas  15249  reopnap  15273  ioo2blex  15279  blssioo  15280  tgioo  15281  fsumcncntop  15294  expcn  15296  cncfval  15299  divccncfap  15317  cdivcncfap  15331  divcncfap  15341  maxcncf  15342  mincncf  15343  ivthdec  15371  hoverb  15375  limccnpcntop  15402  dvrecap  15440  elplyd  15468  ply1termlem  15469  ply1term  15470  plymullem1  15475  plyaddlem  15476  plymullem  15477  plycolemc  15485  plyco  15486  plycj  15488  plycn  15489  plyreres  15491  dvply1  15492  dvply2g  15493  pilem3  15510  tanrpcl  15564  cosordlem  15576  ioocosf1o  15581  rpcncxpcl  15629  rpcxpcl  15630  rpabscxpbnd  15667  rplogbcl  15673  sgmnncl  15715  mpodvdsmulf1o  15717  fsumdvdsmul  15718  mersenne  15724  perfectlem2  15727  lgslem1  15732  lgsval  15736  lgscllem  15739  lgsne0  15770  gausslemma2dlem4  15796  lgseisenlem1  15802  lgsquadlem1  15809  lgsquadlem2  15810  2sqlem3  15849  2sqlem8  15855  vtxex  15872  iedgex  15873  edgvalg  15913  edgopval  15916  edgstruct  15918  usgrausgrien  16023  ausgrumgrien  16024  ausgrusgrien  16025  uspgr1ewopdc  16098  usgr2v1e2w  16100  uhgrspansubgrlem  16130  vtxdgfif  16147  vtxdfifiun  16151  1loopgrvd2fi  16159  1loopgrvd0fi  16160  1hevtxdg0fi  16161  1hevtxdg1en  16162  p1evtxdeqfilem  16165  vdegp1bid  16169  wlkex  16179  wlkelvv  16203  clwwlkccat  16255  clwwlknonex2lem1  16291  clwwlknonex2lem2  16292  clwwlknonex2  16293  trlsegvdeglem6  16319  trlsegvdeglem7  16320  trlsegvdegfi  16321  eupth2lem3lem1fi  16322  eupth2lem3lem2fi  16323  eupth2lem3lem5  16326  eupth2lembfi  16331  djucllem  16413  012of  16609  2o01f  16610  nninfsellemeq  16633  qdencn  16648  cvgcmp2nlemabs  16653  trilpolemclim  16657  trilpolemisumle  16659  trilpolemeq1  16661  trilpolemlt1  16662  nconstwlpolemgt0  16685  gfsumval  16697  gfsumsn  16702  gfsumcl  16704