Theorem eqeltrd 2282

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

Syntax hints:   -> wi 4   = wceq 1373   e. wcel 2176

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  eqeltrrd  2283  3eltr4d  2289  eqeltrid  2292  eqeltrdi  2296  ifcldadc  3600  ifcldcd  3608  intab  3914  disjiun  4040  iinexgm  4199  opexg  4273  tfisi  4636  nnpredcl  4672  imain  5357  fvmptd  5662  fvmptdf  5669  fvmptt  5673  elfvmptrab  5677  dffo3  5729  resfunexg  5807  f1oiso2  5898  riota2df  5922  riota5f  5926  ovmpodxf  6073  ovmpodf  6079  offval  6168  ofvalg  6170  offeq  6174  iunexg  6206  oprabexd  6214  fo1stresm  6249  fo2ndresm  6250  oprssdmm  6259  1stdm  6270  1stconst  6309  2ndconst  6310  cnvf1olem  6312  fo2ndf  6315  f1od2  6323  iunon  6372  tfrlemibacc  6414  tfrlemibfn  6416  tfr1onlembacc  6430  tfr1onlembfn  6432  tfrcllembacc  6443  tfrcllembfn  6445  tfrcl  6452  rdgon  6474  frec0g  6485  freccllem  6490  frecfcllem  6492  frecsuclem  6494  oacl  6548  omcl  6549  oeicl  6550  nntr2  6591  mptelixpg  6823  fidifsnen  6969  en2eqpr  7006  unfiin  7025  tpfidceq  7029  ssfirab  7035  fnfi  7040  relcnvfi  7045  fidcenumlemr  7059  elfi2  7076  supclti  7102  supubti  7103  suplubti  7104  supelti  7106  ordiso2  7139  djulclr  7153  djurclr  7154  djulcl  7155  djurcl  7156  djuss  7174  updjudhcoinlf  7184  updjudhcoinrg  7185  ctssdclemn0  7214  ctssdccl  7215  ctssdc  7217  enumctlemm  7218  nninfwlpoimlemg  7279  cardcl  7290  exmidontriimlem2  7336  exmidapne  7374  cc2lem  7380  cc3  7382  addclpi  7442  mulclpi  7443  addclnq  7490  mulclnq  7491  addclnq0  7566  mulclnq0  7567  nqpnq0nq  7568  elnp1st2nd  7591  prarloclemcalc  7617  distrlem1prl  7697  distrlem1pru  7698  ltexprlemopl  7716  ltexprlemopu  7718  ltexprlemfl  7724  ltexprlemrl  7725  ltexprlemfu  7726  ltexprlemru  7727  addcanprlemu  7730  recexprlemloc  7746  aptiprleml  7754  caucvgprprlemopl  7812  suplocexprlemex  7837  addclsr  7868  mulclsr  7869  recexgt0sr  7888  mulextsr1lem  7895  suplocsrlemb  7921  suplocsrlempr  7922  suplocsrlem  7923  axaddcl  7979  axaddrcl  7980  axmulcl  7981  axmulrcl  7982  axcaucvglemval  8012  subcl  8273  cru  8677  aprcl  8721  aptap  8725  divclap  8753  redivclap  8806  diveqap1bd  8911  lbinfcl  9024  cju  9036  nn1m1nn  9056  nnsub  9077  nnnn0addcl  9327  un0addcl  9330  peano2z  9410  peano2zm  9412  zaddcllemneg  9413  zaddcl  9414  nnaddm1cl  9436  nn0n0n1ge2  9445  zdivadd  9464  zdivmul  9465  suprzclex  9473  zneo  9476  peano5uzti  9483  supinfneg  9718  infsupneg  9719  qmulz  9746  qnegcl  9759  qapne  9762  qdivcl  9766  cnref1o  9774  xnegcl  9956  xltnegi  9959  xaddnemnf  9981  xaddnepnf  9982  xnegdi  9992  xnpcan  9996  xltadd1  10000  xposdif  10006  xleaddadd  10011  iccf1o  10128  ige3m2fz  10173  ige2m1fz1  10233  zssinfcl  10377  infssuzex  10378  infssuzcldc  10380  zsupssdc  10383  suprzcl2dc  10384  rebtwn2z  10399  flqcl  10418  flapcl  10420  ceilqcl  10455  intfracq  10467  modqcl  10473  mulqmod0  10477  modqdifz  10483  zmodcl  10491  modfzo0difsn  10542  modsumfzodifsn  10543  frec2uzzd  10547  frec2uzsucd  10548  frec2uzuzd  10549  frecuzrdgrrn  10555  frec2uzrdg  10556  frecuzrdgrcl  10557  frecuzrdgsuc  10561  frecuzrdgrclt  10562  frecuzrdgg  10563  frecuzrdgsuctlem  10570  fzofig  10579  iseqovex  10605  seq3val  10607  seqvalcd  10608  seqf  10611  seqovcd  10614  seq3clss  10618  seq3caopr3  10638  iseqf1olemnab  10648  iseqf1olemqk  10654  iseqf1olemjpcl  10655  iseqf1olemqpcl  10656  iseqf1olemfvp  10657  seq3f1olemqsumkj  10658  seq3f1olemqsum  10660  seq3f1oleml  10663  seq3f1o  10664  seqf1oglem2a  10665  seqf1oglem1  10666  seqf1oglem2  10667  seq3distr  10679  ser0f  10681  ser3le  10684  exp3vallem  10687  exp3val  10688  exp1  10692  expcl2lemap  10698  m1expcl2  10708  expaddzap  10730  sqcl  10747  nnsqcl  10756  qsqcl  10758  zesq  10805  facp1  10877  faccl  10882  facdiv  10885  bcval  10896  bcrpcl  10900  bcp1n  10908  bcpasc  10913  permnn  10918  hashennn  10927  hashcl  10928  lencl  11000  wrdexg  11007  elovmpowrd  11037  lswcl  11046  ccatcl  11052  ccatrn  11068  lswccatn0lsw  11070  s1cl  11078  swrdclg  11106  swrdwrdsymbg  11120  ccatswrd  11126  pfxval  11130  pfxclg  11133  pfxwrdsymbg  11144  ccatpfx  11155  shftlem  11160  ovshftex  11163  shftf  11174  seq3shft  11182  cjth  11190  imval  11194  recl  11197  imcl  11198  crre  11201  remim  11204  reim0b  11206  cvg1nlemcau  11328  uzin2  11331  resqrexlem1arp  11349  resqrexlemp1rp  11350  resqrexlemglsq  11366  resqrexlemga  11367  resqrtcl  11373  abscl  11395  absrpclap  11405  nn0abscl  11429  fzomaxdiflem  11456  fzomaxdif  11457  maxabslemab  11550  maxcl  11554  zmaxcl  11568  minmax  11574  mincl  11575  xrmaxcl  11596  xrmaxaddlem  11604  xrminmax  11609  xrmincl  11610  xrmineqinf  11613  xrminrpcl  11618  reccn2ap  11657  climaddc1  11673  climmulc2  11675  climsubc1  11676  climsubc2  11677  climle  11678  climlec2  11685  climcvg1nlem  11693  sumrbdclem  11721  fsum3cvg  11722  summodclem3  11724  summodclem2a  11725  zsumdc  11728  fsumgcl  11730  fsum3  11731  isumss  11735  fisumss  11736  isumss2  11737  fsum3cvg2  11738  fsum3ser  11741  fsumcl2lem  11742  fsumcllem  11743  fsumadd  11750  sumsnf  11753  fsumsplitsn  11754  isumcl  11769  isummulc2  11770  isumrecl  11773  isumge0  11774  isumadd  11775  fsum2dlemstep  11778  fisumcom2  11782  mptfzshft  11786  fsumrev  11787  fsummulc2  11792  iserabs  11819  isumshft  11834  isumsplit  11835  isum1p  11836  isumrpcl  11838  isumle  11839  isumlessdc  11840  trireciplem  11844  expcnvap0  11846  expcnvre  11847  expcnv  11848  explecnv  11849  geolim  11855  geolim2  11856  geo2lim  11860  cvgratnnlemsumlt  11872  cvgratz  11876  mertenslemub  11878  mertenslemi1  11879  mertenslem2  11880  mertensabs  11881  prodf1f  11887  prodfdivap  11891  prodrbdclem  11915  fproddccvg  11916  prodmodclem3  11919  prodmodclem2a  11920  zproddc  11923  fprodseq  11927  fprodntrivap  11928  prodssdc  11933  fprodmul  11935  prodsnf  11936  fprodsplitdc  11940  fprodunsn  11948  fprodcl2lem  11949  fprodcllem  11950  fprodabs  11960  fprodrev  11963  fprod2dlemstep  11966  fprodcom2fi  11970  fprodsplitsn  11977  efcllemp  12002  ef0lem  12004  efcvgfsum  12011  reefcl  12012  ege2le3  12015  efcj  12017  efaddlem  12018  eftlcvg  12031  eftlcl  12032  reeftlcl  12033  eftlub  12034  efsep  12035  effsumlt  12036  efgt1p2  12039  efgt1p  12040  reeff1  12044  tanclap  12053  resincl  12064  recoscl  12065  retanclap  12066  eirraplem  12121  dvdsval2  12134  fsumdvds  12186  sqoddm1div8z  12230  bitsinv1lem  12305  gcdval  12313  gcdn0cl  12316  gcddvds  12317  divgcdnnr  12330  uzwodc  12391  nn0seqcvgd  12396  ialgrlem1st  12397  ialgrlemconst  12398  algrf  12400  algrp1  12401  eucalgf  12410  eucalglt  12412  lcmval  12418  lcmcllem  12422  lcmgcdlem  12432  cncongr2  12459  sqrt2irrlem  12516  oddpwdclemxy  12524  oddpwdclemdc  12528  qden1elz  12560  phicl2  12569  phimullem  12580  eulerthlemth  12587  prmdiv  12590  odzcllem  12598  pythagtriplem8  12628  pythagtriplem9  12629  pcval  12652  pczcl  12654  pcqcl  12662  dvdsprmpweqle  12693  pcaddlem  12695  pcmptcl  12698  pcmpt  12699  pockthlem  12712  pockthg  12713  zgz  12729  gznegcl  12731  gzcjcl  12732  gzaddcl  12733  gzmulcl  12734  gzabssqcl  12737  4sqlem5  12738  4sqlem4a  12747  mul4sqlem  12749  mul4sq  12750  4sqlemafi  12751  4sqlemffi  12752  4sqleminfi  12753  4sqexercise1  12754  4sqlem16  12762  4sqlem17  12763  ennnfonelemjn  12806  ennnfonelemg  12807  ennnfonelemp1  12810  ctinfomlemom  12831  ctiunctlemfo  12843  nninfdclemcl  12852  nninfdclemf  12853  nninfdclemp1  12854  setsex  12897  strsetsid  12898  strslfv3  12911  ressex  12930  ressbas2d  12933  strressid  12936  tgvalex  13128  ptex  13129  prdsex  13134  prdsval  13138  imasex  13170  imasival  13171  imasbas  13172  imasplusg  13173  imasmulr  13174  imasaddfn  13182  imasaddval  13183  imasaddf  13184  imasmulfn  13185  imasmulval  13186  imasmulf  13187  qusval  13188  qusex  13190  qusaddvallemg  13198  qusaddflemg  13199  qusaddval  13200  qusaddf  13201  qusmulval  13202  qusmulf  13203  mgm1  13235  gsumress  13260  gsumprval  13264  prdsplusgsgrpcl  13279  prdsplusgcl  13311  prdsidlem  13312  pwsmnd  13315  mhmex  13327  subsubm  13348  0subm  13349  mhmeql  13357  gsumwsubmcl  13361  gsumfzcl  13364  grpsubval  13411  grplinv  13415  pwsgrp  13476  qusgrp2  13482  mulgval  13491  mulgex  13492  mulgfng  13493  mulg1  13498  mulgnnp1  13499  mulgnnsubcl  13503  mulgnn0subcl  13504  mulgsubcl  13505  mulgnndir  13520  subgex  13545  subgsubcl  13554  issubgrpd  13560  subsubg  13566  nsgconj  13575  0nsg  13583  triv1nsgd  13587  eqgex  13590  eqger  13593  eqgcpbl  13597  ghmex  13624  ghmpreima  13635  ghmnsgpreima  13638  conjnmz  13648  gsumfzsubmcl  13707  mgpex  13720  rngmgpf  13732  qusrng  13753  mgpf  13806  qusring2  13861  opprex  13868  opprrng  13872  opprring  13874  dvdsrex  13893  opprunitd  13905  dvrvald  13929  dvrcl  13930  unitdvcl  13931  invrpropdg  13944  subsubrng  14009  subrgcrng  14020  subrgsubm  14029  subrgugrp  14035  subsubrg  14040  rnrhmsubrg  14047  aprcotr  14080  rmodislmod  14146  lssvsubcl  14161  islss3  14174  lspex  14190  ellspsn  14212  sraex  14241  rlmlmod  14259  lidlex  14268  rspex  14269  lidl0cl  14278  lidlacl  14279  lidlnegcl  14280  ridl0  14305  ridl1  14306  2idlelbas  14311  cnsubglem  14374  expghmap  14402  mulgrhm  14404  zrhex  14416  znbaslemnn  14434  psrval  14461  psrbagfi  14468  psrbasg  14469  mplsubgfilemm  14493  mplsubgfilemcl  14494  mplsubgfileminv  14495  mplgrpfi  14501  iunopn  14507  toponmax  14530  tgtop  14573  tgiun  14578  tgidm  14579  ntropn  14622  tgrest  14674  restopnb  14686  cnovex  14701  cnclima  14728  txvalex  14759  txtop  14765  tx1cn  14774  tx2cn  14775  txcnp  14776  txcnmpt  14778  txdis1cn  14783  cnmptcom  14803  imasnopn  14804  hmeocnv  14812  hmeores  14820  txhmeo  14824  txswaphmeo  14826  ispsmet  14828  xmetres  14887  metres  14888  blex  14892  xmeter  14941  xmetresbl  14945  mopntopon  14948  isxms2  14957  xmetxp  15012  xmettx  15015  txmetcnp  15023  qtopbasss  15026  qtopbas  15027  reopnap  15051  ioo2blex  15057  blssioo  15058  tgioo  15059  fsumcncntop  15072  expcn  15074  cncfval  15077  divccncfap  15095  cdivcncfap  15109  divcncfap  15119  maxcncf  15120  mincncf  15121  ivthdec  15149  hoverb  15153  limccnpcntop  15180  dvrecap  15218  elplyd  15246  ply1termlem  15247  ply1term  15248  plymullem1  15253  plyaddlem  15254  plymullem  15255  plycolemc  15263  plyco  15264  plycj  15266  plycn  15267  plyreres  15269  dvply1  15270  dvply2g  15271  pilem3  15288  tanrpcl  15342  cosordlem  15354  ioocosf1o  15359  rpcncxpcl  15407  rpcxpcl  15408  rpabscxpbnd  15445  rplogbcl  15451  sgmnncl  15493  mpodvdsmulf1o  15495  fsumdvdsmul  15496  mersenne  15502  perfectlem2  15505  lgslem1  15510  lgsval  15514  lgscllem  15517  lgsne0  15548  gausslemma2dlem4  15574  lgseisenlem1  15580  lgsquadlem1  15587  lgsquadlem2  15588  2sqlem3  15627  2sqlem8  15633  edgvalg  15687  edgopval  15689  edgstruct  15691  djucllem  15773  012of  15967  2o01f  15968  nninfsellemeq  15988  qdencn  16003  cvgcmp2nlemabs  16008  trilpolemclim  16012  trilpolemisumle  16014  trilpolemeq1  16016  trilpolemlt1  16017  nconstwlpolemgt0  16040