Theorem eqeltrd 2311

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 2303	. 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 2205

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 2216

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

This theorem is referenced by:  eqeltrrd  2312  3eltr4d  2318  eqeltrid  2321  eqeltrdi  2325  ifcldadc  3654  ifcldcd  3662  intab  3980  disjiun  4106  iinexgm  4268  opexg  4346  tfisi  4711  nnpredcl  4747  opabssxpd  4788  imain  5440  fvmptd  5760  fvmptdf  5767  fvmptt  5771  elfvmptrab  5775  dffo3  5826  resfunexg  5907  f1oiso2  6002  riota2df  6027  riota5f  6032  ovmpodxf  6181  ovmpodf  6187  offval  6276  ofvalg  6278  offeq  6282  iunexg  6314  oprabexd  6322  fo1stresm  6357  fo2ndresm  6358  oprssdmm  6367  1stdm  6378  1stconst  6419  2ndconst  6420  cnvf1olem  6422  fo2ndf  6425  f1od2  6433  iunon  6517  tfrlemibacc  6559  tfrlemibfn  6561  tfr1onlembacc  6575  tfr1onlembfn  6577  tfrcllembacc  6588  tfrcllembfn  6590  tfrcl  6597  rdgon  6619  frec0g  6630  freccllem  6635  frecfcllem  6637  frecsuclem  6639  oacl  6695  omcl  6696  oeicl  6697  nntr2  6738  mptelixpg  6971  fidifsnen  7127  en2eqpr  7169  unfiin  7188  tpfidceq  7192  ssfirab  7199  fnfi  7205  relcnvfi  7210  fidcenumlemr  7227  snopfsuppdc  7254  fsuppcorn  7256  elfi2  7261  supclti  7291  supubti  7292  suplubti  7293  supelti  7295  ordiso2  7328  djulclr  7342  djurclr  7343  djulcl  7344  djurcl  7345  djuss  7363  updjudhcoinlf  7373  updjudhcoinrg  7374  ctssdclemn0  7403  ctssdccl  7404  ctssdc  7406  enumctlemm  7407  nninfwlpoimlemg  7468  cardcl  7479  exmidontriimlem2  7531  exmidapne  7576  cc2lem  7582  cc3  7584  addclpi  7644  mulclpi  7645  addclnq  7692  mulclnq  7693  addclnq0  7768  mulclnq0  7769  nqpnq0nq  7770  elnp1st2nd  7793  prarloclemcalc  7819  distrlem1prl  7899  distrlem1pru  7900  ltexprlemopl  7918  ltexprlemopu  7920  ltexprlemfl  7926  ltexprlemrl  7927  ltexprlemfu  7928  ltexprlemru  7929  addcanprlemu  7932  recexprlemloc  7948  aptiprleml  7956  caucvgprprlemopl  8014  suplocexprlemex  8039  addclsr  8070  mulclsr  8071  recexgt0sr  8090  mulextsr1lem  8097  suplocsrlemb  8123  suplocsrlempr  8124  suplocsrlem  8125  axaddcl  8181  axaddrcl  8182  axmulcl  8183  axmulrcl  8184  axcaucvglemval  8214  subcl  8474  cru  8878  aprcl  8922  aptap  8926  divclap  8954  redivclap  9007  diveqap1bd  9112  lbinfcl  9225  cju  9237  nn1m1nn  9257  nnsub  9278  nnnn0addcl  9528  un0addcl  9531  peano2z  9615  peano2zm  9617  zaddcllemneg  9618  zaddcl  9619  nnaddm1cl  9641  nn0n0n1ge2  9650  zdivadd  9670  zdivmul  9671  suprzclex  9679  zneo  9682  peano5uzti  9689  supinfneg  9930  infsupneg  9931  qmulz  9958  qnegcl  9971  qapne  9974  qdivcl  9978  cnref1o  9986  xnegcl  10168  xltnegi  10171  xaddnemnf  10193  xaddnepnf  10194  xnegdi  10204  xnpcan  10208  xltadd1  10212  xposdif  10218  xleaddadd  10223  iccf1o  10341  ige3m2fz  10386  ige2m1fz1  10447  zssinfcl  10596  infssuzex  10597  infssuzcldc  10599  zsupssdc  10602  suprzcl2dc  10603  rebtwn2z  10618  flqcl  10637  flapcl  10639  ceilqcl  10674  intfracq  10686  modqcl  10692  mulqmod0  10696  modqdifz  10702  zmodcl  10710  modfzo0difsn  10761  modsumfzodifsn  10762  frec2uzzd  10766  frec2uzsucd  10767  frec2uzuzd  10768  frecuzrdgrrn  10774  frec2uzrdg  10775  frecuzrdgrcl  10776  frecuzrdgsuc  10780  frecuzrdgrclt  10781  frecuzrdgg  10782  frecuzrdgsuctlem  10789  fzofig  10798  iseqovex  10824  seq3val  10826  seqvalcd  10827  seqf  10830  seqovcd  10833  seq3clss  10837  seq3caopr3  10857  iseqf1olemnab  10867  iseqf1olemqk  10873  iseqf1olemjpcl  10874  iseqf1olemqpcl  10875  iseqf1olemfvp  10876  seq3f1olemqsumkj  10877  seq3f1olemqsum  10879  seq3f1oleml  10882  seq3f1o  10883  seqf1oglem2a  10884  seqf1oglem1  10885  seqf1oglem2  10886  seq3distr  10898  ser0f  10900  ser3le  10903  exp3vallem  10906  exp3val  10907  exp1  10911  expcl2lemap  10917  m1expcl2  10927  expaddzap  10949  sqcl  10966  nnsqcl  10975  qsqcl  10977  zesq  11024  facp1  11096  faccl  11101  facdiv  11104  bcval  11115  bcrpcl  11119  bcp1n  11127  bcpasc  11132  permnn  11138  hashennn  11147  hashcl  11148  lencl  11232  wrdexg  11239  elovmpowrd  11270  lswcl  11279  ccatcl  11285  ccatrn  11301  lswccatn0lsw  11303  ccatalpha  11305  s1cl  11313  swrdclg  11346  swrdwrdsymbg  11360  ccatswrd  11366  pfxval  11370  fnpfx  11373  pfxclg  11374  pfxwrdsymbg  11386  ccatpfx  11397  lenrevpfxcctswrd  11408  wrdind  11418  wrd2ind  11419  shftlem  11505  ovshftex  11508  shftf  11519  seq3shft  11527  cjth  11535  imval  11539  recl  11542  imcl  11543  crre  11546  remim  11549  reim0b  11551  cvg1nlemcau  11673  uzin2  11676  resqrexlem1arp  11694  resqrexlemp1rp  11695  resqrexlemglsq  11711  resqrexlemga  11712  resqrtcl  11718  abscl  11740  absrpclap  11750  nn0abscl  11774  fzomaxdiflem  11801  fzomaxdif  11802  maxabslemab  11895  maxcl  11899  zmaxcl  11913  minmax  11919  mincl  11920  xrmaxcl  11941  xrmaxaddlem  11949  xrminmax  11954  xrmincl  11955  xrmineqinf  11958  xrminrpcl  11963  reccn2ap  12002  climaddc1  12018  climmulc2  12020  climsubc1  12021  climsubc2  12022  climle  12023  climlec2  12030  climcvg1nlem  12038  sumrbdclem  12067  fsum3cvg  12068  summodclem3  12070  summodclem2a  12071  zsumdc  12074  fsumgcl  12076  fsum3  12077  isumss  12081  fisumss  12082  isumss2  12083  fsum3cvg2  12084  fsum3ser  12087  fsumcl2lem  12088  fsumcllem  12089  fsumadd  12096  sumsnf  12099  fsumsplitsn  12100  isumcl  12115  isummulc2  12116  isumrecl  12119  isumge0  12120  isumadd  12121  fsum2dlemstep  12124  fisumcom2  12128  mptfzshft  12132  fsumrev  12133  fsummulc2  12138  iserabs  12165  isumshft  12180  isumsplit  12181  isum1p  12182  isumrpcl  12184  isumle  12185  isumlessdc  12186  trireciplem  12190  expcnvap0  12192  expcnvre  12193  expcnv  12194  explecnv  12195  geolim  12201  geolim2  12202  geo2lim  12206  cvgratnnlemsumlt  12218  cvgratz  12222  mertenslemub  12224  mertenslemi1  12225  mertenslem2  12226  mertensabs  12227  prodf1f  12233  prodfdivap  12237  prodrbdclem  12261  fproddccvg  12262  prodmodclem3  12265  prodmodclem2a  12266  zproddc  12269  fprodseq  12273  fprodntrivap  12274  prodssdc  12279  fprodmul  12281  prodsnf  12282  fprodsplitdc  12286  fprodunsn  12294  fprodcl2lem  12295  fprodcllem  12296  fprodabs  12306  fprodrev  12309  fprod2dlemstep  12312  fprodcom2fi  12316  fprodsplitsn  12323  efcllemp  12348  ef0lem  12350  efcvgfsum  12357  reefcl  12358  ege2le3  12361  efcj  12363  efaddlem  12364  eftlcvg  12377  eftlcl  12378  reeftlcl  12379  eftlub  12380  efsep  12381  effsumlt  12382  efgt1p2  12385  efgt1p  12386  reeff1  12390  tanclap  12399  resincl  12410  recoscl  12411  retanclap  12412  eirraplem  12467  dvdsval2  12480  fsumdvds  12532  sqoddm1div8z  12576  bitsinv1lem  12651  gcdval  12659  gcdn0cl  12662  gcddvds  12663  divgcdnnr  12676  uzwodc  12737  nn0seqcvgd  12742  ialgrlem1st  12743  ialgrlemconst  12744  algrf  12746  algrp1  12747  eucalgf  12756  eucalglt  12758  lcmval  12764  lcmcllem  12768  lcmgcdlem  12778  cncongr2  12805  sqrt2irrlem  12862  oddpwdclemxy  12870  oddpwdclemdc  12874  qden1elz  12906  phicl2  12915  phimullem  12926  eulerthlemth  12933  prmdiv  12936  odzcllem  12944  pythagtriplem8  12974  pythagtriplem9  12975  pcval  12998  pczcl  13000  pcqcl  13008  dvdsprmpweqle  13039  pcaddlem  13041  pcmptcl  13044  pcmpt  13045  pockthlem  13058  pockthg  13059  zgz  13075  gznegcl  13077  gzcjcl  13078  gzaddcl  13079  gzmulcl  13080  gzabssqcl  13083  4sqlem5  13084  4sqlem4a  13093  mul4sqlem  13095  mul4sq  13096  4sqlemafi  13097  4sqlemffi  13098  4sqleminfi  13099  4sqexercise1  13100  4sqlem16  13108  4sqlem17  13109  ballotfilemfelz  13151  ennnfonelemjn  13170  ennnfonelemg  13171  ennnfonelemp1  13174  ctinfomlemom  13195  ctiunctlemfo  13207  nninfdclemcl  13216  nninfdclemf  13217  nninfdclemp1  13218  setsex  13261  strsetsid  13262  strslfv3  13275  bassetsnn  13286  ressex  13295  ressbas2d  13298  strressid  13301  tgvalex  13493  ptex  13494  prdsex  13499  prdsval  13503  imasex  13535  imasival  13536  imasbas  13537  imasplusg  13538  imasmulr  13539  imasaddfn  13547  imasaddval  13548  imasaddf  13549  imasmulfn  13550  imasmulval  13551  imasmulf  13552  qusval  13553  qusex  13555  qusaddvallemg  13563  qusaddflemg  13564  qusaddval  13565  qusaddf  13566  qusmulval  13567  qusmulf  13568  mgm1  13600  gsumress  13625  gsumprval  13629  prdsplusgsgrpcl  13644  prdsplusgcl  13676  prdsidlem  13677  pwsmnd  13680  mhmex  13692  subsubm  13713  0subm  13714  mhmeql  13722  gsumwsubmcl  13726  gsumfzcl  13729  grpsubval  13776  grplinv  13780  pwsgrp  13841  qusgrp2  13847  mulgval  13856  mulgex  13857  mulgfng  13858  mulg1  13863  mulgnnp1  13864  mulgnnsubcl  13868  mulgnn0subcl  13869  mulgsubcl  13870  mulgnndir  13885  subgex  13910  subgsubcl  13919  issubgrpd  13925  subsubg  13931  nsgconj  13940  0nsg  13948  triv1nsgd  13952  eqgex  13955  eqger  13958  eqgcpbl  13962  ghmex  13989  ghmpreima  14000  ghmnsgpreima  14003  conjnmz  14013  gsumfzsubmcl  14072  gsumsplit0  14080  mgpex  14086  rngmgpf  14098  qusrng  14119  mgpf  14172  qusring2  14227  opprex  14234  opprrng  14238  opprring  14240  dvdsrex  14260  opprunitd  14272  dvrvald  14296  dvrcl  14297  unitdvcl  14298  invrpropdg  14311  subsubrng  14376  subrgcrng  14387  subrgsubm  14396  subrgugrp  14402  subsubrg  14407  rnrhmsubrg  14414  aprcotr  14448  aprnzr  14450  aprlring  14451  rmodislmod  14516  lssvsubcl  14531  islss3  14544  lspex  14560  ellspsn  14582  sraex  14611  rlmlmod  14629  lidlex  14638  rspex  14639  lidl0cl  14648  lidlacl  14649  lidlnegcl  14650  ridl0  14675  ridl1  14676  2idlelbas  14681  cnsubglem  14744  expghmap  14772  mulgrhm  14774  zrhex  14786  znbaslemnn  14804  psrval  14831  psrbagfi  14840  psrbagcon  14843  psrbasg  14846  mplsubgfilemm  14870  mplsubgfilemcl  14871  mplsubgfileminv  14872  mplgrpfi  14878  iunopn  14884  toponmax  14907  tgtop  14950  tgiun  14955  tgidm  14956  ntropn  14999  tgrest  15051  restopnb  15063  cnovex  15078  cnclima  15105  txvalex  15136  txtop  15142  tx1cn  15151  tx2cn  15152  txcnp  15153  txcnmpt  15155  txdis1cn  15160  cnmptcom  15180  imasnopn  15181  hmeocnv  15189  hmeores  15197  txhmeo  15201  txswaphmeo  15203  ispsmet  15205  xmetres  15264  metres  15265  blex  15269  xmeter  15318  xmetresbl  15322  mopntopon  15325  isxms2  15334  xmetxp  15389  xmettx  15392  txmetcnp  15400  qtopbasss  15403  qtopbas  15404  reopnap  15428  ioo2blex  15434  blssioo  15435  tgioo  15436  fsumcncntop  15449  expcn  15451  cncfval  15454  divccncfap  15472  cdivcncfap  15486  divcncfap  15496  maxcncf  15497  mincncf  15498  ivthdec  15526  hoverb  15530  limccnpcntop  15557  dvrecap  15595  elplyd  15623  ply1termlem  15624  ply1term  15625  plymullem1  15630  plyaddlem  15631  plymullem  15632  plycolemc  15640  plyco  15641  plycj  15643  plycn  15644  plyreres  15646  dvply1  15647  dvply2g  15648  pilem3  15665  tanrpcl  15719  cosordlem  15731  ioocosf1o  15736  rpcncxpcl  15784  rpcxpcl  15785  rpabscxpbnd  15822  rplogbcl  15828  pellexlem1  15862  sgmnncl  15873  mpodvdsmulf1o  15875  fsumdvdsmul  15876  mersenne  15882  perfectlem2  15885  lgslem1  15890  lgsval  15894  lgscllem  15897  lgsne0  15928  gausslemma2dlem4  15954  lgseisenlem1  15960  lgsquadlem1  15967  lgsquadlem2  15968  2sqlem3  16007  2sqlem8  16013  vtxex  16030  iedgex  16031  edgvalg  16071  edgopval  16074  edgstruct  16076  usgrausgrien  16181  ausgrumgrien  16182  ausgrusgrien  16183  uspgr1ewopdc  16256  usgr2v1e2w  16258  uhgrspansubgrlem  16288  vtxdgfif  16305  vtxdfifiun  16309  1loopgrvd2fi  16317  1loopgrvd0fi  16318  1hevtxdg0fi  16319  1hevtxdg1en  16320  p1evtxdeqfilem  16323  vdegp1bid  16327  wlkex  16337  wlkelvv  16361  clwwlkccat  16413  clwwlknonex2lem1  16449  clwwlknonex2lem2  16450  clwwlknonex2  16451  trlsegvdeglem6  16477  trlsegvdeglem7  16478  trlsegvdegfi  16479  eupth2lem3lem1fi  16480  eupth2lem3lem2fi  16481  eupth2lem3lem5  16484  eupth2lembfi  16489  eulerpathprum  16492  depindlem1  16518  depindlem2  16519  djucllem  16589  012of  16784  2o01f  16785  nninfsellemeq  16809  qdencn  16824  cvgcmp2nlemabs  16833  trilpolemclim  16837  trilpolemisumle  16839  trilpolemeq1  16841  trilpolemlt1  16842  nconstwlpolemgt0  16867  gfsumval  16879  gfsumsn  16884  gfsumcl  16887