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  5717  fvmptdf  5724  fvmptt  5728  elfvmptrab  5732  dffo3  5784  resfunexg  5864  f1oiso2  5957  riota2df  5982  riota5f  5987  ovmpodxf  6136  ovmpodf  6142  offval  6232  ofvalg  6234  offeq  6238  iunexg  6270  oprabexd  6278  fo1stresm  6313  fo2ndresm  6314  oprssdmm  6323  1stdm  6334  1stconst  6373  2ndconst  6374  cnvf1olem  6376  fo2ndf  6379  f1od2  6387  iunon  6436  tfrlemibacc  6478  tfrlemibfn  6480  tfr1onlembacc  6494  tfr1onlembfn  6496  tfrcllembacc  6507  tfrcllembfn  6509  tfrcl  6516  rdgon  6538  frec0g  6549  freccllem  6554  frecfcllem  6556  frecsuclem  6558  oacl  6614  omcl  6615  oeicl  6616  nntr2  6657  mptelixpg  6889  fidifsnen  7040  en2eqpr  7080  unfiin  7099  tpfidceq  7103  ssfirab  7109  fnfi  7114  relcnvfi  7119  fidcenumlemr  7133  elfi2  7150  supclti  7176  supubti  7177  suplubti  7178  supelti  7180  ordiso2  7213  djulclr  7227  djurclr  7228  djulcl  7229  djurcl  7230  djuss  7248  updjudhcoinlf  7258  updjudhcoinrg  7259  ctssdclemn0  7288  ctssdccl  7289  ctssdc  7291  enumctlemm  7292  nninfwlpoimlemg  7353  cardcl  7364  exmidontriimlem2  7415  exmidapne  7457  cc2lem  7463  cc3  7465  addclpi  7525  mulclpi  7526  addclnq  7573  mulclnq  7574  addclnq0  7649  mulclnq0  7650  nqpnq0nq  7651  elnp1st2nd  7674  prarloclemcalc  7700  distrlem1prl  7780  distrlem1pru  7781  ltexprlemopl  7799  ltexprlemopu  7801  ltexprlemfl  7807  ltexprlemrl  7808  ltexprlemfu  7809  ltexprlemru  7810  addcanprlemu  7813  recexprlemloc  7829  aptiprleml  7837  caucvgprprlemopl  7895  suplocexprlemex  7920  addclsr  7951  mulclsr  7952  recexgt0sr  7971  mulextsr1lem  7978  suplocsrlemb  8004  suplocsrlempr  8005  suplocsrlem  8006  axaddcl  8062  axaddrcl  8063  axmulcl  8064  axmulrcl  8065  axcaucvglemval  8095  subcl  8356  cru  8760  aprcl  8804  aptap  8808  divclap  8836  redivclap  8889  diveqap1bd  8994  lbinfcl  9107  cju  9119  nn1m1nn  9139  nnsub  9160  nnnn0addcl  9410  un0addcl  9413  peano2z  9493  peano2zm  9495  zaddcllemneg  9496  zaddcl  9497  nnaddm1cl  9519  nn0n0n1ge2  9528  zdivadd  9547  zdivmul  9548  suprzclex  9556  zneo  9559  peano5uzti  9566  supinfneg  9802  infsupneg  9803  qmulz  9830  qnegcl  9843  qapne  9846  qdivcl  9850  cnref1o  9858  xnegcl  10040  xltnegi  10043  xaddnemnf  10065  xaddnepnf  10066  xnegdi  10076  xnpcan  10080  xltadd1  10084  xposdif  10090  xleaddadd  10095  iccf1o  10212  ige3m2fz  10257  ige2m1fz1  10317  zssinfcl  10464  infssuzex  10465  infssuzcldc  10467  zsupssdc  10470  suprzcl2dc  10471  rebtwn2z  10486  flqcl  10505  flapcl  10507  ceilqcl  10542  intfracq  10554  modqcl  10560  mulqmod0  10564  modqdifz  10570  zmodcl  10578  modfzo0difsn  10629  modsumfzodifsn  10630  frec2uzzd  10634  frec2uzsucd  10635  frec2uzuzd  10636  frecuzrdgrrn  10642  frec2uzrdg  10643  frecuzrdgrcl  10644  frecuzrdgsuc  10648  frecuzrdgrclt  10649  frecuzrdgg  10650  frecuzrdgsuctlem  10657  fzofig  10666  iseqovex  10692  seq3val  10694  seqvalcd  10695  seqf  10698  seqovcd  10701  seq3clss  10705  seq3caopr3  10725  iseqf1olemnab  10735  iseqf1olemqk  10741  iseqf1olemjpcl  10742  iseqf1olemqpcl  10743  iseqf1olemfvp  10744  seq3f1olemqsumkj  10745  seq3f1olemqsum  10747  seq3f1oleml  10750  seq3f1o  10751  seqf1oglem2a  10752  seqf1oglem1  10753  seqf1oglem2  10754  seq3distr  10766  ser0f  10768  ser3le  10771  exp3vallem  10774  exp3val  10775  exp1  10779  expcl2lemap  10785  m1expcl2  10795  expaddzap  10817  sqcl  10834  nnsqcl  10843  qsqcl  10845  zesq  10892  facp1  10964  faccl  10969  facdiv  10972  bcval  10983  bcrpcl  10987  bcp1n  10995  bcpasc  11000  permnn  11005  hashennn  11014  hashcl  11015  lencl  11088  wrdexg  11095  elovmpowrd  11126  lswcl  11135  ccatcl  11141  ccatrn  11157  lswccatn0lsw  11159  ccatalpha  11161  s1cl  11169  swrdclg  11198  swrdwrdsymbg  11212  ccatswrd  11218  pfxval  11222  fnpfx  11225  pfxclg  11226  pfxwrdsymbg  11238  ccatpfx  11249  lenrevpfxcctswrd  11260  wrdind  11270  wrd2ind  11271  shftlem  11343  ovshftex  11346  shftf  11357  seq3shft  11365  cjth  11373  imval  11377  recl  11380  imcl  11381  crre  11384  remim  11387  reim0b  11389  cvg1nlemcau  11511  uzin2  11514  resqrexlem1arp  11532  resqrexlemp1rp  11533  resqrexlemglsq  11549  resqrexlemga  11550  resqrtcl  11556  abscl  11578  absrpclap  11588  nn0abscl  11612  fzomaxdiflem  11639  fzomaxdif  11640  maxabslemab  11733  maxcl  11737  zmaxcl  11751  minmax  11757  mincl  11758  xrmaxcl  11779  xrmaxaddlem  11787  xrminmax  11792  xrmincl  11793  xrmineqinf  11796  xrminrpcl  11801  reccn2ap  11840  climaddc1  11856  climmulc2  11858  climsubc1  11859  climsubc2  11860  climle  11861  climlec2  11868  climcvg1nlem  11876  sumrbdclem  11904  fsum3cvg  11905  summodclem3  11907  summodclem2a  11908  zsumdc  11911  fsumgcl  11913  fsum3  11914  isumss  11918  fisumss  11919  isumss2  11920  fsum3cvg2  11921  fsum3ser  11924  fsumcl2lem  11925  fsumcllem  11926  fsumadd  11933  sumsnf  11936  fsumsplitsn  11937  isumcl  11952  isummulc2  11953  isumrecl  11956  isumge0  11957  isumadd  11958  fsum2dlemstep  11961  fisumcom2  11965  mptfzshft  11969  fsumrev  11970  fsummulc2  11975  iserabs  12002  isumshft  12017  isumsplit  12018  isum1p  12019  isumrpcl  12021  isumle  12022  isumlessdc  12023  trireciplem  12027  expcnvap0  12029  expcnvre  12030  expcnv  12031  explecnv  12032  geolim  12038  geolim2  12039  geo2lim  12043  cvgratnnlemsumlt  12055  cvgratz  12059  mertenslemub  12061  mertenslemi1  12062  mertenslem2  12063  mertensabs  12064  prodf1f  12070  prodfdivap  12074  prodrbdclem  12098  fproddccvg  12099  prodmodclem3  12102  prodmodclem2a  12103  zproddc  12106  fprodseq  12110  fprodntrivap  12111  prodssdc  12116  fprodmul  12118  prodsnf  12119  fprodsplitdc  12123  fprodunsn  12131  fprodcl2lem  12132  fprodcllem  12133  fprodabs  12143  fprodrev  12146  fprod2dlemstep  12149  fprodcom2fi  12153  fprodsplitsn  12160  efcllemp  12185  ef0lem  12187  efcvgfsum  12194  reefcl  12195  ege2le3  12198  efcj  12200  efaddlem  12201  eftlcvg  12214  eftlcl  12215  reeftlcl  12216  eftlub  12217  efsep  12218  effsumlt  12219  efgt1p2  12222  efgt1p  12223  reeff1  12227  tanclap  12236  resincl  12247  recoscl  12248  retanclap  12249  eirraplem  12304  dvdsval2  12317  fsumdvds  12369  sqoddm1div8z  12413  bitsinv1lem  12488  gcdval  12496  gcdn0cl  12499  gcddvds  12500  divgcdnnr  12513  uzwodc  12574  nn0seqcvgd  12579  ialgrlem1st  12580  ialgrlemconst  12581  algrf  12583  algrp1  12584  eucalgf  12593  eucalglt  12595  lcmval  12601  lcmcllem  12605  lcmgcdlem  12615  cncongr2  12642  sqrt2irrlem  12699  oddpwdclemxy  12707  oddpwdclemdc  12711  qden1elz  12743  phicl2  12752  phimullem  12763  eulerthlemth  12770  prmdiv  12773  odzcllem  12781  pythagtriplem8  12811  pythagtriplem9  12812  pcval  12835  pczcl  12837  pcqcl  12845  dvdsprmpweqle  12876  pcaddlem  12878  pcmptcl  12881  pcmpt  12882  pockthlem  12895  pockthg  12896  zgz  12912  gznegcl  12914  gzcjcl  12915  gzaddcl  12916  gzmulcl  12917  gzabssqcl  12920  4sqlem5  12921  4sqlem4a  12930  mul4sqlem  12932  mul4sq  12933  4sqlemafi  12934  4sqlemffi  12935  4sqleminfi  12936  4sqexercise1  12937  4sqlem16  12945  4sqlem17  12946  ennnfonelemjn  12989  ennnfonelemg  12990  ennnfonelemp1  12993  ctinfomlemom  13014  ctiunctlemfo  13026  nninfdclemcl  13035  nninfdclemf  13036  nninfdclemp1  13037  setsex  13080  strsetsid  13081  strslfv3  13094  bassetsnn  13105  ressex  13114  ressbas2d  13117  strressid  13120  tgvalex  13312  ptex  13313  prdsex  13318  prdsval  13322  imasex  13354  imasival  13355  imasbas  13356  imasplusg  13357  imasmulr  13358  imasaddfn  13366  imasaddval  13367  imasaddf  13368  imasmulfn  13369  imasmulval  13370  imasmulf  13371  qusval  13372  qusex  13374  qusaddvallemg  13382  qusaddflemg  13383  qusaddval  13384  qusaddf  13385  qusmulval  13386  qusmulf  13387  mgm1  13419  gsumress  13444  gsumprval  13448  prdsplusgsgrpcl  13463  prdsplusgcl  13495  prdsidlem  13496  pwsmnd  13499  mhmex  13511  subsubm  13532  0subm  13533  mhmeql  13541  gsumwsubmcl  13545  gsumfzcl  13548  grpsubval  13595  grplinv  13599  pwsgrp  13660  qusgrp2  13666  mulgval  13675  mulgex  13676  mulgfng  13677  mulg1  13682  mulgnnp1  13683  mulgnnsubcl  13687  mulgnn0subcl  13688  mulgsubcl  13689  mulgnndir  13704  subgex  13729  subgsubcl  13738  issubgrpd  13744  subsubg  13750  nsgconj  13759  0nsg  13767  triv1nsgd  13771  eqgex  13774  eqger  13777  eqgcpbl  13781  ghmex  13808  ghmpreima  13819  ghmnsgpreima  13822  conjnmz  13832  gsumfzsubmcl  13891  mgpex  13904  rngmgpf  13916  qusrng  13937  mgpf  13990  qusring2  14045  opprex  14052  opprrng  14056  opprring  14058  dvdsrex  14078  opprunitd  14090  dvrvald  14114  dvrcl  14115  unitdvcl  14116  invrpropdg  14129  subsubrng  14194  subrgcrng  14205  subrgsubm  14214  subrgugrp  14220  subsubrg  14225  rnrhmsubrg  14232  aprcotr  14265  rmodislmod  14331  lssvsubcl  14346  islss3  14359  lspex  14375  ellspsn  14397  sraex  14426  rlmlmod  14444  lidlex  14453  rspex  14454  lidl0cl  14463  lidlacl  14464  lidlnegcl  14465  ridl0  14490  ridl1  14491  2idlelbas  14496  cnsubglem  14559  expghmap  14587  mulgrhm  14589  zrhex  14601  znbaslemnn  14619  psrval  14646  psrbagfi  14653  psrbasg  14654  mplsubgfilemm  14678  mplsubgfilemcl  14679  mplsubgfileminv  14680  mplgrpfi  14686  iunopn  14692  toponmax  14715  tgtop  14758  tgiun  14763  tgidm  14764  ntropn  14807  tgrest  14859  restopnb  14871  cnovex  14886  cnclima  14913  txvalex  14944  txtop  14950  tx1cn  14959  tx2cn  14960  txcnp  14961  txcnmpt  14963  txdis1cn  14968  cnmptcom  14988  imasnopn  14989  hmeocnv  14997  hmeores  15005  txhmeo  15009  txswaphmeo  15011  ispsmet  15013  xmetres  15072  metres  15073  blex  15077  xmeter  15126  xmetresbl  15130  mopntopon  15133  isxms2  15142  xmetxp  15197  xmettx  15200  txmetcnp  15208  qtopbasss  15211  qtopbas  15212  reopnap  15236  ioo2blex  15242  blssioo  15243  tgioo  15244  fsumcncntop  15257  expcn  15259  cncfval  15262  divccncfap  15280  cdivcncfap  15294  divcncfap  15304  maxcncf  15305  mincncf  15306  ivthdec  15334  hoverb  15338  limccnpcntop  15365  dvrecap  15403  elplyd  15431  ply1termlem  15432  ply1term  15433  plymullem1  15438  plyaddlem  15439  plymullem  15440  plycolemc  15448  plyco  15449  plycj  15451  plycn  15452  plyreres  15454  dvply1  15455  dvply2g  15456  pilem3  15473  tanrpcl  15527  cosordlem  15539  ioocosf1o  15544  rpcncxpcl  15592  rpcxpcl  15593  rpabscxpbnd  15630  rplogbcl  15636  sgmnncl  15678  mpodvdsmulf1o  15680  fsumdvdsmul  15681  mersenne  15687  perfectlem2  15690  lgslem1  15695  lgsval  15699  lgscllem  15702  lgsne0  15733  gausslemma2dlem4  15759  lgseisenlem1  15765  lgsquadlem1  15772  lgsquadlem2  15773  2sqlem3  15812  2sqlem8  15818  vtxex  15835  iedgex  15836  edgvalg  15876  edgopval  15878  edgstruct  15880  usgrausgrien  15983  ausgrumgrien  15984  ausgrusgrien  15985  vtxdgfif  16053  vtxdfifiun  16057  wlkex  16071  wlkelvv  16095  clwwlkccat  16144  djucllem  16247  012of  16444  2o01f  16445  nninfsellemeq  16468  qdencn  16483  cvgcmp2nlemabs  16488  trilpolemclim  16492  trilpolemisumle  16494  trilpolemeq1  16496  trilpolemlt1  16497  nconstwlpolemgt0  16520