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 )

Syntax hints:   -> wi 4   = wceq 1402   e. wcel 2209

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

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

This theorem is referenced by:  eqeltrrd  2316  3eltr4d  2322  eqeltrid  2325  eqeltrdi  2329  ifcldadc  3670  ifcldcd  3678  intab  3997  disjiun  4123  iinexgm  4288  opexg  4366  tfisi  4732  nnpredcl  4768  opabssxpd  4809  imain  5461  fvmptd  5783  fvmptdf  5790  fvmptt  5794  elfvmptrab  5798  dffo3  5849  resfunexg  5930  f1oiso2  6026  riota2df  6053  riota5f  6058  ovmpodxf  6207  ovmpodf  6213  offval  6303  ofvalg  6305  offeq  6309  iunexg  6341  oprabexd  6353  fo1stresm  6388  fo2ndresm  6389  oprssdmm  6398  1stdm  6409  1stconst  6450  2ndconst  6451  cnvf1olem  6453  fo2ndf  6456  f1od2  6464  iunon  6548  tfrlemibacc  6590  tfrlemibfn  6592  tfr1onlembacc  6606  tfr1onlembfn  6608  tfrcllembacc  6619  tfrcllembfn  6621  tfrcl  6628  rdgon  6650  frec0g  6661  freccllem  6666  frecfcllem  6668  frecsuclem  6670  oacl  6726  omcl  6727  oeicl  6728  nntr2  6769  mptelixpg  7009  fidifsnen  7165  en2eqpr  7207  unfiin  7226  tpfidceq  7230  ssfirab  7237  fnfi  7243  relcnvfi  7248  fidcenumlemr  7265  snopfsuppdc  7292  fsuppcorn  7294  elfi2  7299  supclti  7331  supubti  7332  suplubti  7333  supelti  7335  ordiso2  7368  djulclr  7382  djurclr  7383  djulcl  7384  djurcl  7385  djuss  7403  updjudhcoinlf  7413  updjudhcoinrg  7414  ctssdclemn0  7443  ctssdccl  7444  ctssdc  7446  enumctlemm  7447  nninfwlpoimlemg  7508  cardcl  7519  exmidontriimlem2  7571  exmidapne  7619  cc2lem  7625  cc3  7627  addclpi  7687  mulclpi  7688  addclnq  7735  mulclnq  7736  addclnq0  7811  mulclnq0  7812  nqpnq0nq  7813  elnp1st2nd  7836  prarloclemcalc  7862  distrlem1prl  7942  distrlem1pru  7943  ltexprlemopl  7961  ltexprlemopu  7963  ltexprlemfl  7969  ltexprlemrl  7970  ltexprlemfu  7971  ltexprlemru  7972  addcanprlemu  7975  recexprlemloc  7991  aptiprleml  7999  caucvgprprlemopl  8057  suplocexprlemex  8082  addclsr  8113  mulclsr  8114  recexgt0sr  8133  mulextsr1lem  8140  suplocsrlemb  8166  suplocsrlempr  8167  suplocsrlem  8168  axaddcl  8224  axaddrcl  8225  axmulcl  8226  axmulrcl  8227  axcaucvglemval  8257  subcl  8518  cru  8923  aprcl  8967  aptap  8971  divclap  9001  redivclap  9054  diveqap1bd  9159  lbinfcl  9272  cju  9284  nn1m1nn  9304  nnsub  9325  nnnn0addcl  9575  un0addcl  9578  peano2z  9662  peano2zm  9664  zaddcllemneg  9665  zaddcl  9666  nnaddm1cl  9688  nn0n0n1ge2  9697  zdivadd  9717  zdivmul  9718  suprzclex  9726  zneo  9729  peano5uzti  9736  supinfneg  9977  infsupneg  9978  qmulz  10005  qnegcl  10018  qapne  10021  qdivcl  10025  cnref1o  10033  xnegcl  10216  xltnegi  10219  xaddnemnf  10241  xaddnepnf  10242  xnegdi  10252  xnpcan  10256  xltadd1  10260  xposdif  10266  xleaddadd  10271  iccf1o  10389  ige3m2fz  10435  ige2m1fz1  10497  zssinfcl  10646  infssuzex  10647  infssuzcldc  10649  zsupssdc  10654  suprzcl2dc  10655  rebtwn2z  10670  flqcl  10689  flapcl  10691  ceilqcl  10726  intfracq  10738  modqcl  10744  mulqmod0  10748  modqdifz  10754  zmodcl  10762  modfzo0difsn  10813  modsumfzodifsn  10814  frec2uzzd  10818  frec2uzsucd  10819  frec2uzuzd  10820  frecuzrdgrrn  10826  frec2uzrdg  10827  frecuzrdgrcl  10828  frecuzrdgsuc  10832  frecuzrdgrclt  10833  frecuzrdgg  10834  frecuzrdgsuctlem  10841  fzofig  10850  iseqovex  10876  seq3val  10878  seqvalcd  10879  seqf  10882  seqovcd  10885  seq3clss  10889  seq3caopr3  10909  iseqf1olemnab  10919  iseqf1olemqk  10925  iseqf1olemjpcl  10926  iseqf1olemqpcl  10927  iseqf1olemfvp  10928  seq3f1olemqsumkj  10929  seq3f1olemqsum  10931  seq3f1oleml  10934  seq3f1o  10935  seqf1oglem2a  10936  seqf1oglem1  10937  seqf1oglem2  10938  seq3distr  10950  ser0f  10952  ser3le  10955  exp3vallem  10958  exp3val  10959  exp1  10963  expcl2lemap  10969  m1expcl2  10979  expaddzap  11001  sqcl  11018  nnsqcl  11027  qsqcl  11029  zesq  11077  facp1  11149  faccl  11154  facdiv  11157  bcval  11168  bcrpcl  11172  bcp1n  11180  bcpasc  11185  permnn  11191  hashennn  11200  hashcl  11201  hashf1  11268  lencl  11289  wrdexg  11296  elovmpowrd  11327  lswcl  11336  ccatcl  11342  ccatrn  11358  lswccatn0lsw  11360  ccatalpha  11362  s1cl  11370  swrdclg  11403  swrdwrdsymbg  11417  ccatswrd  11423  pfxval  11427  fnpfx  11430  pfxclg  11431  pfxwrdsymbg  11443  ccatpfx  11454  lenrevpfxcctswrd  11465  wrdind  11475  wrd2ind  11476  shftlem  11562  ovshftex  11565  shftf  11576  seq3shft  11584  cjth  11592  imval  11596  recl  11599  imcl  11600  crre  11603  remim  11606  reim0b  11608  cvg1nlemcau  11731  uzin2  11734  resqrexlem1arp  11752  resqrexlemp1rp  11753  resqrexlemglsq  11769  resqrexlemga  11770  resqrtcl  11776  abscl  11798  absrpclap  11808  nn0abscl  11832  fzomaxdiflem  11859  fzomaxdif  11860  maxabslemab  11953  maxcl  11957  zmaxcl  11971  minmax  11977  mincl  11978  xrmaxcl  11999  xrmaxaddlem  12007  xrminmax  12012  xrmincl  12013  xrmineqinf  12016  xrminrpcl  12021  reccn2ap  12060  climaddc1  12076  climmulc2  12078  climsubc1  12079  climsubc2  12080  climle  12081  climlec2  12088  climcvg1nlem  12096  sumrbdclem  12125  fsum3cvg  12126  summodclem3  12128  summodclem2a  12129  zsumdc  12132  fsumgcl  12134  fsum3  12135  isumss  12139  fisumss  12140  isumss2  12141  fsum3cvg2  12142  fsum3ser  12145  fsumcl2lem  12146  fsumcllem  12147  fsumadd  12154  sumsnf  12157  fsumsplitsn  12158  isumcl  12173  isummulc2  12174  isumrecl  12177  isumge0  12178  isumadd  12179  fsum2dlemstep  12182  fisumcom2  12186  mptfzshft  12190  fsumrev  12191  fsummulc2  12196  iserabs  12223  isumshft  12238  isumsplit  12239  isum1p  12240  isumrpcl  12242  isumle  12243  isumlessdc  12244  trireciplem  12248  expcnvap0  12250  expcnvre  12251  expcnv  12252  explecnv  12253  geolim  12259  geolim2  12260  geo2lim  12264  cvgratnnlemsumlt  12276  cvgratz  12280  mertenslemub  12282  mertenslemi1  12283  mertenslem2  12284  mertensabs  12285  prodf1f  12291  prodfdivap  12295  prodrbdclem  12319  fproddccvg  12320  prodmodclem3  12323  prodmodclem2a  12324  zproddc  12327  fprodseq  12331  fprodntrivap  12332  prodssdc  12337  fprodmul  12339  prodsnf  12340  fprodsplitdc  12344  fprodunsn  12352  fprodcl2lem  12353  fprodcllem  12354  fprodabs  12364  fprodrev  12367  fprod2dlemstep  12370  fprodcom2fi  12374  fprodsplitsn  12381  efcllemp  12406  ef0lem  12408  efcvgfsum  12415  reefcl  12416  ege2le3  12419  efcj  12421  efaddlem  12422  eftlcvg  12435  eftlcl  12436  reeftlcl  12437  eftlub  12438  efsep  12439  effsumlt  12440  efgt1p2  12443  efgt1p  12444  reeff1  12448  tanclap  12457  resincl  12468  recoscl  12469  retanclap  12470  eirraplem  12525  dvdsval2  12538  fsumdvds  12590  sqoddm1div8z  12634  bitsinv1lem  12709  gcdval  12717  gcdn0cl  12720  gcddvds  12721  divgcdnnr  12734  uzwodc  12795  nn0seqcvgd  12800  ialgrlem1st  12801  ialgrlemconst  12802  algrf  12804  algrp1  12805  eucalgf  12814  eucalglt  12816  lcmval  12822  lcmcllem  12826  lcmgcdlem  12836  cncongr2  12863  sqrt2irrlem  12920  oddpwdclemxy  12928  oddpwdclemdc  12932  qden1elz  12964  phicl2  12973  phimullem  12984  eulerthlemth  12991  prmdiv  12994  odzcllem  13002  pythagtriplem8  13032  pythagtriplem9  13033  pcval  13056  pczcl  13058  pcqcl  13066  dvdsprmpweqle  13097  pcaddlem  13099  pcmptcl  13102  pcmpt  13103  pockthlem  13116  pockthg  13117  zgz  13133  gznegcl  13135  gzcjcl  13136  gzaddcl  13137  gzmulcl  13138  gzabssqcl  13141  4sqlem5  13142  4sqlem4a  13151  mul4sqlem  13153  mul4sq  13154  4sqlemafi  13155  4sqlemffi  13156  4sqleminfi  13157  4sqexercise1  13158  4sqlem16  13166  4sqlem17  13167  ballotfilemfelz  13211  ballotfilemiex  13225  ballotfilemsdom  13236  ballotfilemgval  13248  ennnfonelemjn  13274  ennnfonelemg  13275  ennnfonelemp1  13278  ctinfomlemom  13299  ctiunctlemfo  13311  nninfdclemcl  13320  nninfdclemf  13321  nninfdclemp1  13322  setsex  13365  strsetsid  13366  strslfv3  13379  bassetsnn  13390  ressex  13399  ressbas2d  13402  strressid  13405  tgvalex  13597  ptex  13598  imasex  13606  imasival  13607  imasbas  13608  imasplusg  13609  imasmulr  13610  imasaddfn  13618  imasaddval  13619  imasaddf  13620  imasmulfn  13621  imasmulval  13622  imasmulf  13623  qusval  13624  qusex  13626  qusaddvallemg  13634  qusaddflemg  13635  qusaddval  13636  qusaddf  13637  qusmulval  13638  qusmulf  13639  mgm1  13670  gzsumress  13692  mhmex  13749  subsubm  13770  0subm  13771  mhmeql  13779  gzsumwsubmcl  13781  gzsumcl  13784  grpsubval  13831  grplinv  13835  qusgrp2  13896  mulgval  13905  mulgex  13906  mulgfng  13907  mulg1  13912  mulgnnp1  13913  mulgnnsubcl  13917  mulgnn0subcl  13918  mulgsubcl  13919  mulgnndir  13934  subgex  13959  subgsubcl  13968  issubgrpd  13974  subsubg  13980  nsgconj  13989  0nsg  13997  triv1nsgd  14001  eqgex  14004  eqger  14007  eqgcpbl  14011  ghmex  14038  ghmpreima  14049  ghmnsgpreima  14052  conjnmz  14062  gzsumsubmcl  14122  gzsumsplit0  14128  gsumvalfi  14132  gsumsncmn  14136  gsumclfi  14139  gsumsubmclfi  14143  prdsex  14152  prdsval  14153  prdsplusgsgrpcl  14170  prdsplusgcl  14172  prdsidlem  14173  pwsmnd  14192  pwsgrp  14194  mgpex  14202  rngmgpf  14214  qusrng  14235  mgpf  14292  qusring2  14347  opprex  14354  opprrng  14358  opprring  14360  dvdsrex  14381  opprunitd  14393  dvrvald  14417  dvrcl  14418  unitdvcl  14419  invrpropdg  14432  subsubrng  14498  subrgcrng  14509  subrgsubm  14518  subrgugrp  14524  subsubrg  14529  rnrhmsubrg  14536  aprcotr  14573  aprnzr  14575  aprlring  14576  rmodislmod  14663  lssvsubcl  14678  islss3  14691  lspex  14707  ellspsn  14729  sraex  14758  rlmlmod  14776  lidlex  14785  rspex  14786  lidl0cl  14795  lidlacl  14796  lidlnegcl  14797  ridl0  14822  ridl1  14823  2idlelbas  14828  cnsubglem  14891  expghmap  14917  mulgrhm  14919  zrhex  14931  znbaslemnn  14949  psrval  14976  psrbagfi  14985  psrbagcon  14988  psrbasg  14991  mplsubgfilemm  15015  mplsubgfilemcl  15016  mplsubgfileminv  15017  mplgrpfi  15023  iunopn  15029  toponmax  15052  tgtop  15095  tgiun  15100  tgidm  15101  ntropn  15144  tgrest  15196  restopnb  15208  cnovex  15223  cnclima  15250  txvalex  15281  txtop  15287  tx1cn  15296  tx2cn  15297  txcnp  15298  txcnmpt  15300  txdis1cn  15305  cnmptcom  15325  imasnopn  15326  hmeocnv  15334  hmeores  15342  txhmeo  15346  txswaphmeo  15348  ispsmet  15350  xmetres  15409  metres  15410  blex  15414  xmeter  15463  xmetresbl  15467  mopntopon  15470  isxms2  15479  xmetxp  15534  xmettx  15537  txmetcnp  15545  qtopbasss  15548  qtopbas  15549  reopnap  15573  ioo2blex  15579  blssioo  15580  tgioo  15581  fsumcncntop  15594  expcn  15596  cncfval  15599  divccncfap  15617  cdivcncfap  15631  divcncfap  15641  maxcncf  15642  mincncf  15643  ivthdec  15671  hoverb  15675  limccnpcntop  15702  dvrecap  15740  elplyd  15768  ply1termlem  15769  ply1term  15770  plymullem1  15775  plyaddlem  15776  plymullem  15777  plycolemc  15785  plyco  15786  plycj  15788  plycn  15789  plyreres  15791  dvply1  15792  dvply2g  15793  pilem3  15810  tanrpcl  15864  cosordlem  15876  ioocosf1o  15881  logfac  15921  rpcncxpcl  15930  rpcxpcl  15931  rpabscxpbnd  15968  rplogbcl  15974  pellexlem1  16008  sgmnncl  16019  mpodvdsmulf1o  16021  fsumdvdsmul  16022  mersenne  16028  perfectlem2  16031  lgslem1  16036  lgsval  16040  lgscllem  16043  lgsne0  16074  gausslemma2dlem4  16100  lgseisenlem1  16106  lgsquadlem1  16113  lgsquadlem2  16114  2sqlem3  16153  2sqlem8  16159  vtxex  16176  iedgex  16177  edgvalg  16217  edgopval  16220  edgstruct  16222  usgrausgrien  16327  ausgrumgrien  16328  ausgrusgrien  16329  uspgr1ewopdc  16402  usgr2v1e2w  16404  uhgrspansubgrlem  16434  vtxdgfif  16451  vtxdfifiun  16455  1loopgrvd2fi  16463  1loopgrvd0fi  16464  1hevtxdg0fi  16465  1hevtxdg1en  16466  p1evtxdeqfilem  16469  vdegp1bid  16473  wlkex  16483  wlkelvv  16507  clwwlkccat  16559  clwwlknonex2lem1  16595  clwwlknonex2lem2  16596  clwwlknonex2  16597  trlsegvdeglem6  16623  trlsegvdeglem7  16624  trlsegvdegfi  16625  eupth2lem3lem1fi  16626  eupth2lem3lem2fi  16627  eupth2lem3lem5  16630  eupth2lembfi  16635  eulerpathprum  16638  depindlem1  16664  depindlem2  16665  djucllem  16745  012of  16940  2o01f  16941  nninfsellemeq  16965  qdencn  16980  cvgcmp2nlemabs  16989  trilpolemclim  16993  trilpolemisumle  16995  trilpolemeq1  16997  trilpolemlt1  16998  nconstwlpolemgt0  17022