Theorem eqeltrd 2315

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   e. wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  eqeltrrd  2316  3eltr4d  2322  eqeltrid  2325  eqeltrdi  2329  ifcldadc  3670  ifcldcd  3678  intab  3999  disjiun  4125  iinexgm  4290  opexg  4368  tfisi  4734  nnpredcl  4770  opabssxpd  4811  imain  5463  fvmptd  5786  fvmptdf  5793  fvmptt  5797  elfvmptrab  5802  dffo3  5855  resfunexg  5936  f1oiso2  6033  riota2df  6060  riota5f  6065  ovmpodxf  6214  ovmpodf  6220  offval  6310  ofvalg  6312  offeq  6316  iunexg  6348  oprabexd  6360  fo1stresm  6395  fo2ndresm  6396  oprssdmm  6405  1stdm  6416  1stconst  6457  2ndconst  6458  cnvf1olem  6460  fo2ndf  6463  f1od2  6471  iunon  6555  tfrlemibacc  6597  tfrlemibfn  6599  tfr1onlembacc  6613  tfr1onlembfn  6615  tfrcllembacc  6626  tfrcllembfn  6628  tfrcl  6635  rdgon  6657  frec0g  6668  freccllem  6673  frecfcllem  6675  frecsuclem  6677  oacl  6733  omcl  6734  oeicl  6735  nntr2  6776  mptelixpg  7016  fidifsnen  7172  en2eqpr  7214  unfiin  7233  tpfidceq  7237  ssfirab  7244  fnfi  7250  relcnvfi  7255  fidcenumlemr  7272  snopfsuppdc  7299  fsuppcorn  7301  elfi2  7306  supclti  7338  supubti  7339  suplubti  7340  supelti  7342  ordiso2  7375  djulclr  7389  djurclr  7390  djulcl  7391  djurcl  7392  djuss  7410  updjudhcoinlf  7420  updjudhcoinrg  7421  ctssdclemn0  7450  ctssdccl  7451  ctssdc  7453  enumctlemm  7454  nninfwlpoimlemg  7515  cardcl  7526  exmidontriimlem2  7578  exmidapne  7626  cc2lem  7632  cc3  7634  addclpi  7694  mulclpi  7695  addclnq  7742  mulclnq  7743  addclnq0  7818  mulclnq0  7819  nqpnq0nq  7820  elnp1st2nd  7843  prarloclemcalc  7869  distrlem1prl  7949  distrlem1pru  7950  ltexprlemopl  7968  ltexprlemopu  7970  ltexprlemfl  7976  ltexprlemrl  7977  ltexprlemfu  7978  ltexprlemru  7979  addcanprlemu  7982  recexprlemloc  7998  aptiprleml  8006  caucvgprprlemopl  8064  suplocexprlemex  8089  addclsr  8120  mulclsr  8121  recexgt0sr  8140  mulextsr1lem  8147  suplocsrlemb  8173  suplocsrlempr  8174  suplocsrlem  8175  axaddcl  8231  axaddrcl  8232  axmulcl  8233  axmulrcl  8234  axcaucvglemval  8264  subcl  8525  cru  8930  aprcl  8974  aptap  8978  divclap  9008  redivclap  9061  diveqap1bd  9166  lbinfcl  9279  cju  9291  nn1m1nn  9322  nnsub  9343  nnnn0addcl  9593  un0addcl  9596  peano2z  9680  peano2zm  9682  zaddcllemneg  9683  zaddcl  9684  nnaddm1cl  9706  nn0n0n1ge2  9715  zdivadd  9735  zdivmul  9736  suprzclex  9744  zneo  9747  peano5uzti  9754  supinfneg  9995  infsupneg  9996  qmulz  10023  qnegcl  10036  qapne  10039  qdivcl  10043  cnref1o  10051  xnegcl  10234  xltnegi  10237  xaddnemnf  10259  xaddnepnf  10260  xnegdi  10270  xnpcan  10274  xltadd1  10278  xposdif  10284  xleaddadd  10289  iccf1o  10407  ige3m2fz  10454  ige2m1fz1  10516  zssinfcl  10665  infssuzex  10666  infssuzcldc  10668  zsupssdc  10673  suprzcl2dc  10674  rebtwn2z  10689  flqcl  10708  flapcl  10710  ceilqcl  10745  intfracq  10757  modqcl  10763  mulqmod0  10767  modqdifz  10773  zmodcl  10781  modfzo0difsn  10832  modsumfzodifsn  10833  frec2uzzd  10837  frec2uzsucd  10838  frec2uzuzd  10839  frecuzrdgrrn  10845  frec2uzrdg  10846  frecuzrdgrcl  10847  frecuzrdgsuc  10851  frecuzrdgrclt  10852  frecuzrdgg  10853  frecuzrdgsuctlem  10860  fzofig  10869  iseqovex  10895  seq3val  10897  seqvalcd  10898  seqf  10901  seqovcd  10904  seq3clss  10908  seq3caopr3  10928  iseqf1olemnab  10938  iseqf1olemqk  10944  iseqf1olemjpcl  10945  iseqf1olemqpcl  10946  iseqf1olemfvp  10947  seq3f1olemqsumkj  10948  seq3f1olemqsum  10950  seq3f1oleml  10953  seq3f1o  10954  seqf1oglem2a  10955  seqf1oglem1  10956  seqf1oglem2  10957  seq3distr  10969  ser0f  10971  ser3le  10974  exp3vallem  10977  exp3val  10978  exp1  10982  expcl2lemap  10988  m1expcl2  10998  expaddzap  11020  sqcl  11037  nnsqcl  11046  qsqcl  11048  zesq  11096  facp1  11168  faccl  11173  facdiv  11176  bcval  11187  bcrpcl  11191  bcp1n  11199  bcpasc  11204  permnn  11210  hashennn  11219  hashcl  11220  hashf1  11287  lencl  11308  wrdexg  11315  elovmpowrd  11346  lswcl  11355  ccatcl  11361  ccatrn  11377  lswccatn0lsw  11379  ccatalpha  11381  s1cl  11389  swrdclg  11422  swrdwrdsymbg  11436  ccatswrd  11442  pfxval  11446  fnpfx  11449  pfxclg  11450  pfxwrdsymbg  11462  ccatpfx  11473  lenrevpfxcctswrd  11484  wrdind  11494  wrd2ind  11495  shftlem  11581  ovshftex  11584  shftf  11595  seq3shft  11603  cjth  11611  imval  11615  recl  11618  imcl  11619  crre  11622  remim  11625  reim0b  11627  cvg1nlemcau  11750  uzin2  11753  resqrexlem1arp  11771  resqrexlemp1rp  11772  resqrexlemglsq  11788  resqrexlemga  11789  resqrtcl  11795  abscl  11817  absrpclap  11827  nn0abscl  11851  fzomaxdiflem  11878  fzomaxdif  11879  maxabslemab  11972  maxcl  11976  zmaxcl  11990  minmax  11996  mincl  11997  xrmaxcl  12018  xrmaxaddlem  12026  xrminmax  12031  xrmincl  12032  xrmineqinf  12035  xrminrpcl  12040  reccn2ap  12079  climaddc1  12095  climmulc2  12097  climsubc1  12098  climsubc2  12099  climle  12100  climlec2  12107  climcvg1nlem  12115  sumrbdclem  12144  fsum3cvg  12145  summodclem3  12147  summodclem2a  12148  zsumdc  12151  fsumgcl  12153  fsum3  12154  isumss  12158  fisumss  12159  isumss2  12160  fsum3cvg2  12161  fsum3ser  12164  fsumcl2lem  12165  fsumcllem  12166  fsumadd  12173  sumsnf  12176  fsumsplitsn  12177  isumcl  12192  isummulc2  12193  isumrecl  12196  isumge0  12197  isumadd  12198  fsum2dlemstep  12201  fisumcom2  12205  mptfzshft  12209  fsumrev  12210  fsummulc2  12215  iserabs  12242  isumshft  12257  isumsplit  12258  isum1p  12259  isumrpcl  12261  isumle  12262  isumlessdc  12263  trireciplem  12267  expcnvap0  12269  expcnvre  12270  expcnv  12271  explecnv  12272  geolim  12278  geolim2  12279  geo2lim  12283  cvgratnnlemsumlt  12295  cvgratz  12299  mertenslemub  12301  mertenslemi1  12302  mertenslem2  12303  mertensabs  12304  prodf1f  12310  prodfdivap  12314  prodrbdclem  12338  fproddccvg  12339  prodmodclem3  12342  prodmodclem2a  12343  zproddc  12346  fprodseq  12350  fprodntrivap  12351  prodssdc  12356  fprodmul  12358  prodsnf  12359  fprodsplitdc  12363  fprodunsn  12371  fprodcl2lem  12372  fprodcllem  12373  fprodabs  12383  fprodrev  12386  fprod2dlemstep  12389  fprodcom2fi  12393  fprodsplitsn  12400  efcllemp  12425  ef0lem  12427  efcvgfsum  12434  reefcl  12435  ege2le3  12438  efcj  12440  efaddlem  12441  eftlcvg  12454  eftlcl  12455  reeftlcl  12456  eftlub  12457  efsep  12458  effsumlt  12459  efgt1p2  12462  efgt1p  12463  reeff1  12467  tanclap  12476  resincl  12487  recoscl  12488  retanclap  12489  eirraplem  12544  dvdsval2  12557  fsumdvds  12609  sqoddm1div8z  12653  bitsinv1lem  12728  gcdval  12736  gcdn0cl  12739  gcddvds  12740  divgcdnnr  12753  uzwodc  12814  nn0seqcvgd  12819  ialgrlem1st  12820  ialgrlemconst  12821  algrf  12823  algrp1  12824  eucalgf  12833  eucalglt  12835  lcmval  12841  lcmcllem  12845  lcmgcdlem  12855  cncongr2  12882  sqrt2irrlem  12939  oddpwdclemxy  12947  oddpwdclemdc  12951  qden1elz  12983  phicl2  12992  phimullem  13003  eulerthlemth  13010  prmdiv  13013  odzcllem  13021  pythagtriplem8  13051  pythagtriplem9  13052  pcval  13075  pczcl  13077  pcqcl  13085  dvdsprmpweqle  13116  pcaddlem  13118  pcmptcl  13121  pcmpt  13122  pockthlem  13135  pockthg  13136  zgz  13152  gznegcl  13154  gzcjcl  13155  gzaddcl  13156  gzmulcl  13157  gzabssqcl  13160  4sqlem5  13161  4sqlem4a  13170  mul4sqlem  13172  mul4sq  13173  4sqlemafi  13174  4sqlemffi  13175  4sqleminfi  13176  4sqexercise1  13177  4sqlem16  13185  4sqlem17  13186  ballotfilemfelz  13230  ballotfilemiex  13244  ballotfilemsdom  13255  ballotfilemgval  13267  ennnfonelemjn  13293  ennnfonelemg  13294  ennnfonelemp1  13297  ctinfomlemom  13318  ctiunctlemfo  13330  nninfdclemcl  13339  nninfdclemf  13340  nninfdclemp1  13341  setsex  13384  strsetsid  13385  strslfv3  13398  bassetsnn  13409  ressex  13419  ressbas2d  13422  strressid  13425  tgvalex  13617  ptex  13618  imasex  13626  imasival  13627  imasbas  13628  imasplusg  13629  imasmulr  13630  imasaddfn  13638  imasaddval  13639  imasaddf  13640  imasmulfn  13641  imasmulval  13642  imasmulf  13643  qusval  13644  qusex  13646  qusaddvallemg  13654  qusaddflemg  13655  qusaddval  13656  qusaddf  13657  qusmulval  13658  qusmulf  13659  mgm1  13690  gzsumress  13712  mhmex  13769  subsubm  13790  0subm  13791  mhmeql  13799  gzsumwsubmcl  13801  gzsumcl  13804  grpsubval  13851  grplinv  13855  qusgrp2  13916  mulgval  13925  mulgex  13926  mulgfng  13927  mulg1  13932  mulgnnp1  13933  mulgnnsubcl  13937  mulgnn0subcl  13938  mulgsubcl  13939  mulgnndir  13954  subgex  13979  subgsubcl  13988  issubgrpd  13994  subsubg  14000  nsgconj  14009  0nsg  14017  triv1nsgd  14021  eqgex  14024  eqger  14027  eqgcpbl  14031  ghmex  14058  ghmpreima  14069  ghmnsgpreima  14072  conjnmz  14082  gzsumsubmcl  14142  gzsumsplit0  14148  gsumvalfi  14152  gsumsncmn  14156  gsumclfi  14159  gsumsubmclfi  14163  prdsex  14172  prdsval  14173  prdsplusgsgrpcl  14190  prdsplusgcl  14192  prdsidlem  14193  pwsmnd  14212  pwsgrp  14214  mgpex  14223  rngmgpf  14236  qusrng  14257  mgpf  14315  qusring2  14371  opprex  14378  opprrng  14382  opprring  14384  dvdsrex  14405  opprunitd  14417  dvrvald  14441  dvrcl  14442  unitdvcl  14443  invrpropdg  14456  subsubrng  14522  subrgcrng  14533  subrgsubm  14542  subrgugrp  14548  subsubrg  14553  rnrhmsubrg  14560  aprcotr  14597  aprnzr  14599  aprlring  14600  rmodislmod  14688  lssvsubcl  14703  islss3  14716  lspex  14732  ellspsn  14754  sraex  14783  rlmlmod  14801  lidlex  14810  rspex  14811  lidl0cl  14820  lidlacl  14821  lidlnegcl  14822  ridl0  14847  ridl1  14848  2idlelbas  14853  cnsubglem  14916  expghmap  14942  mulgrhm  14944  zrhex  14956  znbaslemnn  14974  asplss  15016  aspsubrg  15018  psrval  15050  psrbagfi  15059  psrbagcon  15062  psrbasg  15065  mplsubgfilemm  15089  mplsubgfilemcl  15090  mplsubgfileminv  15091  mplgrpfi  15097  iunopn  15103  toponmax  15126  tgtop  15169  tgiun  15174  tgidm  15175  ntropn  15218  tgrest  15270  restopnb  15282  cnovex  15297  cnclima  15324  txvalex  15355  txtop  15361  tx1cn  15370  tx2cn  15371  txcnp  15372  txcnmpt  15374  txdis1cn  15379  cnmptcom  15399  imasnopn  15400  hmeocnv  15408  hmeores  15416  txhmeo  15420  txswaphmeo  15422  ispsmet  15424  xmetres  15483  metres  15484  blex  15488  xmeter  15537  xmetresbl  15541  mopntopon  15544  isxms2  15553  xmetxp  15608  xmettx  15611  txmetcnp  15619  qtopbasss  15622  qtopbas  15623  reopnap  15647  ioo2blex  15653  blssioo  15654  tgioo  15655  fsumcncntop  15668  expcn  15670  cncfval  15673  divccncfap  15691  cdivcncfap  15705  divcncfap  15715  maxcncf  15716  mincncf  15717  ivthdec  15745  hoverb  15749  limccnpcntop  15776  dvrecap  15814  elplyd  15842  ply1termlem  15843  ply1term  15844  plymullem1  15849  plyaddlem  15850  plymullem  15851  plycolemc  15859  plyco  15860  plycj  15862  plycn  15863  plyreres  15865  dvply1  15866  dvply2g  15867  pilem3  15884  tanrpcl  15938  cosordlem  15950  ioocosf1o  15955  logfac  15995  rpcncxpcl  16004  rpcxpcl  16005  rpabscxpbnd  16042  rplogbcl  16048  log2tlbndlog2  16082  birthdaylem1g  16087  pellexlem1  16091  sgmnncl  16102  mpodvdsmulf1o  16104  fsumdvdsmul  16105  mersenne  16111  perfectlem2  16114  lgslem1  16119  lgsval  16123  lgscllem  16126  lgsne0  16157  gausslemma2dlem4  16183  lgseisenlem1  16189  lgsquadlem1  16196  lgsquadlem2  16197  2sqlem3  16236  2sqlem8  16242  vtxex  16259  iedgex  16260  edgvalg  16300  edgopval  16303  edgstruct  16305  usgrausgrien  16410  ausgrumgrien  16411  ausgrusgrien  16412  uspgr1ewopdc  16485  usgr2v1e2w  16487  uhgrspansubgrlem  16517  vtxdgfif  16534  vtxdfifiun  16538  1loopgrvd2fi  16546  1loopgrvd0fi  16547  1hevtxdg0fi  16548  1hevtxdg1en  16549  p1evtxdeqfilem  16552  vdegp1bid  16556  wlkex  16566  wlkelvv  16590  clwwlkccat  16642  clwwlknonex2lem1  16678  clwwlknonex2lem2  16679  clwwlknonex2  16680  trlsegvdeglem6  16706  trlsegvdeglem7  16707  trlsegvdegfi  16708  eupth2lem3lem1fi  16709  eupth2lem3lem2fi  16710  eupth2lem3lem5  16713  eupth2lembfi  16718  eulerpathprum  16721  depindlem1  16747  depindlem2  16748  djucllem  16828  012of  17023  2o01f  17024  nninfsellemeq  17057  qdencn  17072  cvgcmp2nlemabs  17081  trilpolemclim  17085  trilpolemisumle  17087  trilpolemeq1  17089  trilpolemlt1  17090  nconstwlpolemgt0  17114