Theorem eqeltrd 2306

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 2298	. 2 |- ( ph -> ( A e. C <-> B e. C ) )
4	1, 3	mpbird 167	1 |- ( ph -> A e. C )

Syntax hints:   -> wi 4   = wceq 1395   e. wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  eqeltrrd  2307  3eltr4d  2313  eqeltrid  2316  eqeltrdi  2320  ifcldadc  3632  ifcldcd  3640  intab  3952  disjiun  4078  iinexgm  4238  opexg  4314  tfisi  4679  nnpredcl  4715  imain  5403  fvmptd  5715  fvmptdf  5722  fvmptt  5726  elfvmptrab  5730  dffo3  5782  resfunexg  5860  f1oiso2  5951  riota2df  5976  riota5f  5981  ovmpodxf  6130  ovmpodf  6136  offval  6226  ofvalg  6228  offeq  6232  iunexg  6264  oprabexd  6272  fo1stresm  6307  fo2ndresm  6308  oprssdmm  6317  1stdm  6328  1stconst  6367  2ndconst  6368  cnvf1olem  6370  fo2ndf  6373  f1od2  6381  iunon  6430  tfrlemibacc  6472  tfrlemibfn  6474  tfr1onlembacc  6488  tfr1onlembfn  6490  tfrcllembacc  6501  tfrcllembfn  6503  tfrcl  6510  rdgon  6532  frec0g  6543  freccllem  6548  frecfcllem  6550  frecsuclem  6552  oacl  6606  omcl  6607  oeicl  6608  nntr2  6649  mptelixpg  6881  fidifsnen  7032  en2eqpr  7069  unfiin  7088  tpfidceq  7092  ssfirab  7098  fnfi  7103  relcnvfi  7108  fidcenumlemr  7122  elfi2  7139  supclti  7165  supubti  7166  suplubti  7167  supelti  7169  ordiso2  7202  djulclr  7216  djurclr  7217  djulcl  7218  djurcl  7219  djuss  7237  updjudhcoinlf  7247  updjudhcoinrg  7248  ctssdclemn0  7277  ctssdccl  7278  ctssdc  7280  enumctlemm  7281  nninfwlpoimlemg  7342  cardcl  7353  exmidontriimlem2  7404  exmidapne  7446  cc2lem  7452  cc3  7454  addclpi  7514  mulclpi  7515  addclnq  7562  mulclnq  7563  addclnq0  7638  mulclnq0  7639  nqpnq0nq  7640  elnp1st2nd  7663  prarloclemcalc  7689  distrlem1prl  7769  distrlem1pru  7770  ltexprlemopl  7788  ltexprlemopu  7790  ltexprlemfl  7796  ltexprlemrl  7797  ltexprlemfu  7798  ltexprlemru  7799  addcanprlemu  7802  recexprlemloc  7818  aptiprleml  7826  caucvgprprlemopl  7884  suplocexprlemex  7909  addclsr  7940  mulclsr  7941  recexgt0sr  7960  mulextsr1lem  7967  suplocsrlemb  7993  suplocsrlempr  7994  suplocsrlem  7995  axaddcl  8051  axaddrcl  8052  axmulcl  8053  axmulrcl  8054  axcaucvglemval  8084  subcl  8345  cru  8749  aprcl  8793  aptap  8797  divclap  8825  redivclap  8878  diveqap1bd  8983  lbinfcl  9096  cju  9108  nn1m1nn  9128  nnsub  9149  nnnn0addcl  9399  un0addcl  9402  peano2z  9482  peano2zm  9484  zaddcllemneg  9485  zaddcl  9486  nnaddm1cl  9508  nn0n0n1ge2  9517  zdivadd  9536  zdivmul  9537  suprzclex  9545  zneo  9548  peano5uzti  9555  supinfneg  9790  infsupneg  9791  qmulz  9818  qnegcl  9831  qapne  9834  qdivcl  9838  cnref1o  9846  xnegcl  10028  xltnegi  10031  xaddnemnf  10053  xaddnepnf  10054  xnegdi  10064  xnpcan  10068  xltadd1  10072  xposdif  10078  xleaddadd  10083  iccf1o  10200  ige3m2fz  10245  ige2m1fz1  10305  zssinfcl  10452  infssuzex  10453  infssuzcldc  10455  zsupssdc  10458  suprzcl2dc  10459  rebtwn2z  10474  flqcl  10493  flapcl  10495  ceilqcl  10530  intfracq  10542  modqcl  10548  mulqmod0  10552  modqdifz  10558  zmodcl  10566  modfzo0difsn  10617  modsumfzodifsn  10618  frec2uzzd  10622  frec2uzsucd  10623  frec2uzuzd  10624  frecuzrdgrrn  10630  frec2uzrdg  10631  frecuzrdgrcl  10632  frecuzrdgsuc  10636  frecuzrdgrclt  10637  frecuzrdgg  10638  frecuzrdgsuctlem  10645  fzofig  10654  iseqovex  10680  seq3val  10682  seqvalcd  10683  seqf  10686  seqovcd  10689  seq3clss  10693  seq3caopr3  10713  iseqf1olemnab  10723  iseqf1olemqk  10729  iseqf1olemjpcl  10730  iseqf1olemqpcl  10731  iseqf1olemfvp  10732  seq3f1olemqsumkj  10733  seq3f1olemqsum  10735  seq3f1oleml  10738  seq3f1o  10739  seqf1oglem2a  10740  seqf1oglem1  10741  seqf1oglem2  10742  seq3distr  10754  ser0f  10756  ser3le  10759  exp3vallem  10762  exp3val  10763  exp1  10767  expcl2lemap  10773  m1expcl2  10783  expaddzap  10805  sqcl  10822  nnsqcl  10831  qsqcl  10833  zesq  10880  facp1  10952  faccl  10957  facdiv  10960  bcval  10971  bcrpcl  10975  bcp1n  10983  bcpasc  10988  permnn  10993  hashennn  11002  hashcl  11003  lencl  11075  wrdexg  11082  elovmpowrd  11113  lswcl  11122  ccatcl  11128  ccatrn  11144  lswccatn0lsw  11146  s1cl  11154  swrdclg  11182  swrdwrdsymbg  11196  ccatswrd  11202  pfxval  11206  fnpfx  11209  pfxclg  11210  pfxwrdsymbg  11222  ccatpfx  11233  lenrevpfxcctswrd  11244  wrdind  11254  wrd2ind  11255  shftlem  11327  ovshftex  11330  shftf  11341  seq3shft  11349  cjth  11357  imval  11361  recl  11364  imcl  11365  crre  11368  remim  11371  reim0b  11373  cvg1nlemcau  11495  uzin2  11498  resqrexlem1arp  11516  resqrexlemp1rp  11517  resqrexlemglsq  11533  resqrexlemga  11534  resqrtcl  11540  abscl  11562  absrpclap  11572  nn0abscl  11596  fzomaxdiflem  11623  fzomaxdif  11624  maxabslemab  11717  maxcl  11721  zmaxcl  11735  minmax  11741  mincl  11742  xrmaxcl  11763  xrmaxaddlem  11771  xrminmax  11776  xrmincl  11777  xrmineqinf  11780  xrminrpcl  11785  reccn2ap  11824  climaddc1  11840  climmulc2  11842  climsubc1  11843  climsubc2  11844  climle  11845  climlec2  11852  climcvg1nlem  11860  sumrbdclem  11888  fsum3cvg  11889  summodclem3  11891  summodclem2a  11892  zsumdc  11895  fsumgcl  11897  fsum3  11898  isumss  11902  fisumss  11903  isumss2  11904  fsum3cvg2  11905  fsum3ser  11908  fsumcl2lem  11909  fsumcllem  11910  fsumadd  11917  sumsnf  11920  fsumsplitsn  11921  isumcl  11936  isummulc2  11937  isumrecl  11940  isumge0  11941  isumadd  11942  fsum2dlemstep  11945  fisumcom2  11949  mptfzshft  11953  fsumrev  11954  fsummulc2  11959  iserabs  11986  isumshft  12001  isumsplit  12002  isum1p  12003  isumrpcl  12005  isumle  12006  isumlessdc  12007  trireciplem  12011  expcnvap0  12013  expcnvre  12014  expcnv  12015  explecnv  12016  geolim  12022  geolim2  12023  geo2lim  12027  cvgratnnlemsumlt  12039  cvgratz  12043  mertenslemub  12045  mertenslemi1  12046  mertenslem2  12047  mertensabs  12048  prodf1f  12054  prodfdivap  12058  prodrbdclem  12082  fproddccvg  12083  prodmodclem3  12086  prodmodclem2a  12087  zproddc  12090  fprodseq  12094  fprodntrivap  12095  prodssdc  12100  fprodmul  12102  prodsnf  12103  fprodsplitdc  12107  fprodunsn  12115  fprodcl2lem  12116  fprodcllem  12117  fprodabs  12127  fprodrev  12130  fprod2dlemstep  12133  fprodcom2fi  12137  fprodsplitsn  12144  efcllemp  12169  ef0lem  12171  efcvgfsum  12178  reefcl  12179  ege2le3  12182  efcj  12184  efaddlem  12185  eftlcvg  12198  eftlcl  12199  reeftlcl  12200  eftlub  12201  efsep  12202  effsumlt  12203  efgt1p2  12206  efgt1p  12207  reeff1  12211  tanclap  12220  resincl  12231  recoscl  12232  retanclap  12233  eirraplem  12288  dvdsval2  12301  fsumdvds  12353  sqoddm1div8z  12397  bitsinv1lem  12472  gcdval  12480  gcdn0cl  12483  gcddvds  12484  divgcdnnr  12497  uzwodc  12558  nn0seqcvgd  12563  ialgrlem1st  12564  ialgrlemconst  12565  algrf  12567  algrp1  12568  eucalgf  12577  eucalglt  12579  lcmval  12585  lcmcllem  12589  lcmgcdlem  12599  cncongr2  12626  sqrt2irrlem  12683  oddpwdclemxy  12691  oddpwdclemdc  12695  qden1elz  12727  phicl2  12736  phimullem  12747  eulerthlemth  12754  prmdiv  12757  odzcllem  12765  pythagtriplem8  12795  pythagtriplem9  12796  pcval  12819  pczcl  12821  pcqcl  12829  dvdsprmpweqle  12860  pcaddlem  12862  pcmptcl  12865  pcmpt  12866  pockthlem  12879  pockthg  12880  zgz  12896  gznegcl  12898  gzcjcl  12899  gzaddcl  12900  gzmulcl  12901  gzabssqcl  12904  4sqlem5  12905  4sqlem4a  12914  mul4sqlem  12916  mul4sq  12917  4sqlemafi  12918  4sqlemffi  12919  4sqleminfi  12920  4sqexercise1  12921  4sqlem16  12929  4sqlem17  12930  ennnfonelemjn  12973  ennnfonelemg  12974  ennnfonelemp1  12977  ctinfomlemom  12998  ctiunctlemfo  13010  nninfdclemcl  13019  nninfdclemf  13020  nninfdclemp1  13021  setsex  13064  strsetsid  13065  strslfv3  13078  bassetsnn  13089  ressex  13098  ressbas2d  13101  strressid  13104  tgvalex  13296  ptex  13297  prdsex  13302  prdsval  13306  imasex  13338  imasival  13339  imasbas  13340  imasplusg  13341  imasmulr  13342  imasaddfn  13350  imasaddval  13351  imasaddf  13352  imasmulfn  13353  imasmulval  13354  imasmulf  13355  qusval  13356  qusex  13358  qusaddvallemg  13366  qusaddflemg  13367  qusaddval  13368  qusaddf  13369  qusmulval  13370  qusmulf  13371  mgm1  13403  gsumress  13428  gsumprval  13432  prdsplusgsgrpcl  13447  prdsplusgcl  13479  prdsidlem  13480  pwsmnd  13483  mhmex  13495  subsubm  13516  0subm  13517  mhmeql  13525  gsumwsubmcl  13529  gsumfzcl  13532  grpsubval  13579  grplinv  13583  pwsgrp  13644  qusgrp2  13650  mulgval  13659  mulgex  13660  mulgfng  13661  mulg1  13666  mulgnnp1  13667  mulgnnsubcl  13671  mulgnn0subcl  13672  mulgsubcl  13673  mulgnndir  13688  subgex  13713  subgsubcl  13722  issubgrpd  13728  subsubg  13734  nsgconj  13743  0nsg  13751  triv1nsgd  13755  eqgex  13758  eqger  13761  eqgcpbl  13765  ghmex  13792  ghmpreima  13803  ghmnsgpreima  13806  conjnmz  13816  gsumfzsubmcl  13875  mgpex  13888  rngmgpf  13900  qusrng  13921  mgpf  13974  qusring2  14029  opprex  14036  opprrng  14040  opprring  14042  dvdsrex  14062  opprunitd  14074  dvrvald  14098  dvrcl  14099  unitdvcl  14100  invrpropdg  14113  subsubrng  14178  subrgcrng  14189  subrgsubm  14198  subrgugrp  14204  subsubrg  14209  rnrhmsubrg  14216  aprcotr  14249  rmodislmod  14315  lssvsubcl  14330  islss3  14343  lspex  14359  ellspsn  14381  sraex  14410  rlmlmod  14428  lidlex  14437  rspex  14438  lidl0cl  14447  lidlacl  14448  lidlnegcl  14449  ridl0  14474  ridl1  14475  2idlelbas  14480  cnsubglem  14543  expghmap  14571  mulgrhm  14573  zrhex  14585  znbaslemnn  14603  psrval  14630  psrbagfi  14637  psrbasg  14638  mplsubgfilemm  14662  mplsubgfilemcl  14663  mplsubgfileminv  14664  mplgrpfi  14670  iunopn  14676  toponmax  14699  tgtop  14742  tgiun  14747  tgidm  14748  ntropn  14791  tgrest  14843  restopnb  14855  cnovex  14870  cnclima  14897  txvalex  14928  txtop  14934  tx1cn  14943  tx2cn  14944  txcnp  14945  txcnmpt  14947  txdis1cn  14952  cnmptcom  14972  imasnopn  14973  hmeocnv  14981  hmeores  14989  txhmeo  14993  txswaphmeo  14995  ispsmet  14997  xmetres  15056  metres  15057  blex  15061  xmeter  15110  xmetresbl  15114  mopntopon  15117  isxms2  15126  xmetxp  15181  xmettx  15184  txmetcnp  15192  qtopbasss  15195  qtopbas  15196  reopnap  15220  ioo2blex  15226  blssioo  15227  tgioo  15228  fsumcncntop  15241  expcn  15243  cncfval  15246  divccncfap  15264  cdivcncfap  15278  divcncfap  15288  maxcncf  15289  mincncf  15290  ivthdec  15318  hoverb  15322  limccnpcntop  15349  dvrecap  15387  elplyd  15415  ply1termlem  15416  ply1term  15417  plymullem1  15422  plyaddlem  15423  plymullem  15424  plycolemc  15432  plyco  15433  plycj  15435  plycn  15436  plyreres  15438  dvply1  15439  dvply2g  15440  pilem3  15457  tanrpcl  15511  cosordlem  15523  ioocosf1o  15528  rpcncxpcl  15576  rpcxpcl  15577  rpabscxpbnd  15614  rplogbcl  15620  sgmnncl  15662  mpodvdsmulf1o  15664  fsumdvdsmul  15665  mersenne  15671  perfectlem2  15674  lgslem1  15679  lgsval  15683  lgscllem  15686  lgsne0  15717  gausslemma2dlem4  15743  lgseisenlem1  15749  lgsquadlem1  15756  lgsquadlem2  15757  2sqlem3  15796  2sqlem8  15802  vtxex  15819  iedgex  15820  edgvalg  15860  edgopval  15862  edgstruct  15864  usgrausgrien  15967  ausgrumgrien  15968  ausgrusgrien  15969  wlkelvv  16060  djucllem  16164  012of  16357  2o01f  16358  nninfsellemeq  16380  qdencn  16395  cvgcmp2nlemabs  16400  trilpolemclim  16404  trilpolemisumle  16406  trilpolemeq1  16408  trilpolemlt1  16409  nconstwlpolemgt0  16432