Theorem eqeltrd 2266

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

Syntax hints:   -> wi 4   = wceq 1364   e. wcel 2160

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-cleq 2182  df-clel 2185

This theorem is referenced by:  eqeltrrd  2267  3eltr4d  2273  eqeltrid  2276  eqeltrdi  2280  ifcldadc  3578  ifcldcd  3585  intab  3888  disjiun  4013  iinexgm  4169  opexg  4243  tfisi  4601  nnpredcl  4637  imain  5313  fvmptd  5613  fvmptdf  5619  fvmptt  5623  elfvmptrab  5627  dffo3  5679  resfunexg  5753  f1oiso2  5844  riota2df  5867  riota5f  5871  ovmpodxf  6017  ovmpodf  6023  offval  6108  ofvalg  6110  offeq  6114  iunexg  6138  oprabexd  6146  fo1stresm  6180  fo2ndresm  6181  oprssdmm  6190  1stdm  6201  1stconst  6240  2ndconst  6241  cnvf1olem  6243  fo2ndf  6246  f1od2  6254  iunon  6303  tfrlemibacc  6345  tfrlemibfn  6347  tfr1onlembacc  6361  tfr1onlembfn  6363  tfrcllembacc  6374  tfrcllembfn  6376  tfrcl  6383  rdgon  6405  frec0g  6416  freccllem  6421  frecfcllem  6423  frecsuclem  6425  oacl  6479  omcl  6480  oeicl  6481  nntr2  6522  mptelixpg  6752  fidifsnen  6888  en2eqpr  6925  unfiin  6943  ssfirab  6951  fnfi  6954  relcnvfi  6958  fidcenumlemr  6972  elfi2  6989  supclti  7015  supubti  7016  suplubti  7017  supelti  7019  ordiso2  7052  djulclr  7066  djurclr  7067  djulcl  7068  djurcl  7069  djuss  7087  updjudhcoinlf  7097  updjudhcoinrg  7098  ctssdclemn0  7127  ctssdccl  7128  ctssdc  7130  enumctlemm  7131  nninfwlpoimlemg  7191  cardcl  7198  exmidontriimlem2  7239  exmidapne  7277  cc2lem  7283  cc3  7285  addclpi  7344  mulclpi  7345  addclnq  7392  mulclnq  7393  addclnq0  7468  mulclnq0  7469  nqpnq0nq  7470  elnp1st2nd  7493  prarloclemcalc  7519  distrlem1prl  7599  distrlem1pru  7600  ltexprlemopl  7618  ltexprlemopu  7620  ltexprlemfl  7626  ltexprlemrl  7627  ltexprlemfu  7628  ltexprlemru  7629  addcanprlemu  7632  recexprlemloc  7648  aptiprleml  7656  caucvgprprlemopl  7714  suplocexprlemex  7739  addclsr  7770  mulclsr  7771  recexgt0sr  7790  mulextsr1lem  7797  suplocsrlemb  7823  suplocsrlempr  7824  suplocsrlem  7825  axaddcl  7881  axaddrcl  7882  axmulcl  7883  axmulrcl  7884  axcaucvglemval  7914  subcl  8174  cru  8577  aprcl  8621  aptap  8625  divclap  8653  redivclap  8706  diveqap1bd  8811  lbinfcl  8924  cju  8936  nn1m1nn  8955  nnsub  8976  nnnn0addcl  9224  un0addcl  9227  peano2z  9307  peano2zm  9309  zaddcllemneg  9310  zaddcl  9311  nnaddm1cl  9332  nn0n0n1ge2  9341  zdivadd  9360  zdivmul  9361  suprzclex  9369  zneo  9372  peano5uzti  9379  supinfneg  9613  infsupneg  9614  qmulz  9641  qnegcl  9654  qapne  9657  qdivcl  9661  cnref1o  9668  xnegcl  9850  xltnegi  9853  xaddnemnf  9875  xaddnepnf  9876  xnegdi  9886  xnpcan  9890  xltadd1  9894  xposdif  9900  xleaddadd  9905  iccf1o  10022  ige3m2fz  10067  ige2m1fz1  10127  rebtwn2z  10273  flqcl  10291  flapcl  10293  ceilqcl  10326  intfracq  10338  modqcl  10344  mulqmod0  10348  modqdifz  10354  zmodcl  10362  modfzo0difsn  10413  modsumfzodifsn  10414  frec2uzzd  10418  frec2uzsucd  10419  frec2uzuzd  10420  frecuzrdgrrn  10426  frec2uzrdg  10427  frecuzrdgrcl  10428  frecuzrdgsuc  10432  frecuzrdgrclt  10433  frecuzrdgg  10434  frecuzrdgsuctlem  10441  fzofig  10450  iseqovex  10474  seq3val  10476  seqvalcd  10477  seqf  10479  seqovcd  10481  seq3clss  10485  seq3caopr3  10499  iseqf1olemnab  10506  iseqf1olemqk  10512  iseqf1olemjpcl  10513  iseqf1olemqpcl  10514  iseqf1olemfvp  10515  seq3f1olemqsumkj  10516  seq3f1olemqsum  10518  seq3f1oleml  10521  seq3f1o  10522  seq3distr  10531  ser0f  10533  ser3le  10536  exp3vallem  10539  exp3val  10540  exp1  10544  expcl2lemap  10550  m1expcl2  10560  expaddzap  10582  sqcl  10599  nnsqcl  10608  qsqcl  10610  zesq  10657  facp1  10728  faccl  10733  facdiv  10736  bcval  10747  bcrpcl  10751  bcp1n  10759  bcpasc  10764  permnn  10769  hashennn  10778  hashcl  10779  shftlem  10843  ovshftex  10846  shftf  10857  seq3shft  10865  cjth  10873  imval  10877  recl  10880  imcl  10881  crre  10884  remim  10887  reim0b  10889  cvg1nlemcau  11011  uzin2  11014  resqrexlem1arp  11032  resqrexlemp1rp  11033  resqrexlemglsq  11049  resqrexlemga  11050  resqrtcl  11056  abscl  11078  absrpclap  11088  nn0abscl  11112  fzomaxdiflem  11139  fzomaxdif  11140  maxabslemab  11233  maxcl  11237  zmaxcl  11251  minmax  11256  mincl  11257  xrmaxcl  11278  xrmaxaddlem  11286  xrminmax  11291  xrmincl  11292  xrmineqinf  11295  xrminrpcl  11300  reccn2ap  11339  climaddc1  11355  climmulc2  11357  climsubc1  11358  climsubc2  11359  climle  11360  climlec2  11367  climcvg1nlem  11375  sumrbdclem  11403  fsum3cvg  11404  summodclem3  11406  summodclem2a  11407  zsumdc  11410  fsumgcl  11412  fsum3  11413  isumss  11417  fisumss  11418  isumss2  11419  fsum3cvg2  11420  fsum3ser  11423  fsumcl2lem  11424  fsumcllem  11425  fsumadd  11432  sumsnf  11435  fsumsplitsn  11436  isumcl  11451  isummulc2  11452  isumrecl  11455  isumge0  11456  isumadd  11457  fsum2dlemstep  11460  fisumcom2  11464  mptfzshft  11468  fsumrev  11469  fsummulc2  11474  iserabs  11501  isumshft  11516  isumsplit  11517  isum1p  11518  isumrpcl  11520  isumle  11521  isumlessdc  11522  trireciplem  11526  expcnvap0  11528  expcnvre  11529  expcnv  11530  explecnv  11531  geolim  11537  geolim2  11538  geo2lim  11542  cvgratnnlemsumlt  11554  cvgratz  11558  mertenslemub  11560  mertenslemi1  11561  mertenslem2  11562  mertensabs  11563  prodf1f  11569  prodfdivap  11573  prodrbdclem  11597  fproddccvg  11598  prodmodclem3  11601  prodmodclem2a  11602  zproddc  11605  fprodseq  11609  fprodntrivap  11610  prodssdc  11615  fprodmul  11617  prodsnf  11618  fprodsplitdc  11622  fprodunsn  11630  fprodcl2lem  11631  fprodcllem  11632  fprodabs  11642  fprodrev  11645  fprod2dlemstep  11648  fprodcom2fi  11652  fprodsplitsn  11659  efcllemp  11684  ef0lem  11686  efcvgfsum  11693  reefcl  11694  ege2le3  11697  efcj  11699  efaddlem  11700  eftlcvg  11713  eftlcl  11714  reeftlcl  11715  eftlub  11716  efsep  11717  effsumlt  11718  efgt1p2  11721  efgt1p  11722  reeff1  11726  tanclap  11735  resincl  11746  recoscl  11747  retanclap  11748  eirraplem  11802  dvdsval2  11815  sqoddm1div8z  11909  zssinfcl  11967  infssuzex  11968  infssuzcldc  11970  zsupssdc  11973  suprzcl2dc  11974  gcdval  11978  gcdn0cl  11981  gcddvds  11982  divgcdnnr  11995  uzwodc  12056  nn0seqcvgd  12059  ialgrlem1st  12060  ialgrlemconst  12061  algrf  12063  algrp1  12064  eucalgf  12073  eucalglt  12075  lcmval  12081  lcmcllem  12085  lcmgcdlem  12095  cncongr2  12122  sqrt2irrlem  12179  oddpwdclemxy  12187  oddpwdclemdc  12191  qden1elz  12223  phicl2  12232  phimullem  12243  eulerthlemth  12250  prmdiv  12253  odzcllem  12260  pythagtriplem8  12290  pythagtriplem9  12291  pcval  12314  pczcl  12316  pcqcl  12324  dvdsprmpweqle  12354  pcaddlem  12356  pcmptcl  12358  pcmpt  12359  pockthlem  12372  pockthg  12373  zgz  12389  gznegcl  12391  gzcjcl  12392  gzaddcl  12393  gzmulcl  12394  gzabssqcl  12397  4sqlem5  12398  4sqlem4a  12407  mul4sqlem  12409  mul4sq  12410  ennnfonelemjn  12421  ennnfonelemg  12422  ennnfonelemp1  12425  ctinfomlemom  12446  ctiunctlemfo  12458  nninfdclemcl  12467  nninfdclemf  12468  nninfdclemp1  12469  setsex  12512  strsetsid  12513  ressex  12543  ressbas2d  12546  strressid  12549  tgvalex  12734  ptex  12735  prdsex  12740  imasex  12748  imasival  12749  imasbas  12750  imasplusg  12751  imasmulr  12752  imasaddfn  12760  imasaddval  12761  imasaddf  12762  imasmulfn  12763  imasmulval  12764  imasmulf  12765  qusval  12766  qusex  12768  qusaddvallemg  12775  qusaddflemg  12776  qusaddval  12777  qusaddf  12778  qusmulval  12779  qusmulf  12780  mgm1  12812  mhmex  12880  subsubm  12901  0subm  12902  mhmeql  12910  grpsubval  12956  grplinv  12960  qusgrp2  13021  mulgval  13030  mulgex  13031  mulgfng  13032  mulg1  13035  mulgnnp1  13036  mulgnnsubcl  13040  mulgnn0subcl  13041  mulgsubcl  13042  mulgnndir  13057  subgex  13081  subgsubcl  13090  issubgrpd  13096  subsubg  13102  nsgconj  13111  0nsg  13119  triv1nsgd  13123  eqgex  13126  eqger  13129  eqgcpbl  13133  ghmex  13155  ghmpreima  13166  ghmnsgpreima  13169  conjnmz  13179  mgpex  13240  rngmgpf  13252  qusrng  13273  mgpf  13326  qusring2  13377  opprex  13384  opprrng  13388  opprring  13390  dvdsrex  13409  opprunitd  13421  dvrvald  13445  dvrcl  13446  unitdvcl  13447  invrpropdg  13460  subsubrng  13522  subrgcrng  13533  subrgsubm  13542  subrgugrp  13548  subsubrg  13553  aprcotr  13562  rmodislmod  13628  lssvsubcl  13643  islss3  13656  lspex  13672  lspsnel  13694  sraex  13723  rlmlmod  13741  lidlex  13750  rspex  13751  lidl0cl  13760  lidlacl  13761  lidlnegcl  13762  ridl0  13786  ridl1  13787  2idlelbas  13792  cnsubglem  13843  iunopn  13886  toponmax  13909  tgtop  13952  tgiun  13957  tgidm  13958  ntropn  14001  tgrest  14053  restopnb  14065  cnovex  14080  cnclima  14107  txvalex  14138  txtop  14144  tx1cn  14153  tx2cn  14154  txcnp  14155  txcnmpt  14157  txdis1cn  14162  cnmptcom  14182  imasnopn  14183  hmeocnv  14191  hmeores  14199  txhmeo  14203  txswaphmeo  14205  ispsmet  14207  xmetres  14266  metres  14267  blex  14271  xmeter  14320  xmetresbl  14324  mopntopon  14327  isxms2  14336  xmetxp  14391  xmettx  14394  txmetcnp  14402  qtopbasss  14405  qtopbas  14406  reopnap  14422  ioo2blex  14428  blssioo  14429  tgioo  14430  fsumcncntop  14440  cncfval  14443  divccncfap  14461  cdivcncfap  14471  ivthdec  14506  limccnpcntop  14528  dvrecap  14561  pilem3  14588  tanrpcl  14642  cosordlem  14654  ioocosf1o  14659  rpcncxpcl  14707  rpcxpcl  14708  rpabscxpbnd  14743  rplogbcl  14748  lgslem1  14785  lgsval  14789  lgscllem  14792  lgsne0  14823  lgseisenlem1  14834  2sqlem3  14848  2sqlem8  14854  djucllem  14936  012of  15130  2o01f  15131  nninfsellemeq  15148  qdencn  15160  cvgcmp2nlemabs  15165  trilpolemclim  15169  trilpolemisumle  15171  trilpolemeq1  15173  trilpolemlt1  15174  nconstwlpolemgt0  15197