Theorem eqeltrd 2273

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 2265	. 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 2167

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  eqeltrrd  2274  3eltr4d  2280  eqeltrid  2283  eqeltrdi  2287  ifcldadc  3591  ifcldcd  3598  intab  3904  disjiun  4029  iinexgm  4188  opexg  4262  tfisi  4624  nnpredcl  4660  imain  5341  fvmptd  5645  fvmptdf  5652  fvmptt  5656  elfvmptrab  5660  dffo3  5712  resfunexg  5786  f1oiso2  5877  riota2df  5901  riota5f  5905  ovmpodxf  6052  ovmpodf  6058  offval  6147  ofvalg  6149  offeq  6153  iunexg  6185  oprabexd  6193  fo1stresm  6228  fo2ndresm  6229  oprssdmm  6238  1stdm  6249  1stconst  6288  2ndconst  6289  cnvf1olem  6291  fo2ndf  6294  f1od2  6302  iunon  6351  tfrlemibacc  6393  tfrlemibfn  6395  tfr1onlembacc  6409  tfr1onlembfn  6411  tfrcllembacc  6422  tfrcllembfn  6424  tfrcl  6431  rdgon  6453  frec0g  6464  freccllem  6469  frecfcllem  6471  frecsuclem  6473  oacl  6527  omcl  6528  oeicl  6529  nntr2  6570  mptelixpg  6802  fidifsnen  6940  en2eqpr  6977  unfiin  6996  tpfidceq  7000  ssfirab  7006  fnfi  7011  relcnvfi  7016  fidcenumlemr  7030  elfi2  7047  supclti  7073  supubti  7074  suplubti  7075  supelti  7077  ordiso2  7110  djulclr  7124  djurclr  7125  djulcl  7126  djurcl  7127  djuss  7145  updjudhcoinlf  7155  updjudhcoinrg  7156  ctssdclemn0  7185  ctssdccl  7186  ctssdc  7188  enumctlemm  7189  nninfwlpoimlemg  7250  cardcl  7259  exmidontriimlem2  7305  exmidapne  7343  cc2lem  7349  cc3  7351  addclpi  7411  mulclpi  7412  addclnq  7459  mulclnq  7460  addclnq0  7535  mulclnq0  7536  nqpnq0nq  7537  elnp1st2nd  7560  prarloclemcalc  7586  distrlem1prl  7666  distrlem1pru  7667  ltexprlemopl  7685  ltexprlemopu  7687  ltexprlemfl  7693  ltexprlemrl  7694  ltexprlemfu  7695  ltexprlemru  7696  addcanprlemu  7699  recexprlemloc  7715  aptiprleml  7723  caucvgprprlemopl  7781  suplocexprlemex  7806  addclsr  7837  mulclsr  7838  recexgt0sr  7857  mulextsr1lem  7864  suplocsrlemb  7890  suplocsrlempr  7891  suplocsrlem  7892  axaddcl  7948  axaddrcl  7949  axmulcl  7950  axmulrcl  7951  axcaucvglemval  7981  subcl  8242  cru  8646  aprcl  8690  aptap  8694  divclap  8722  redivclap  8775  diveqap1bd  8880  lbinfcl  8993  cju  9005  nn1m1nn  9025  nnsub  9046  nnnn0addcl  9296  un0addcl  9299  peano2z  9379  peano2zm  9381  zaddcllemneg  9382  zaddcl  9383  nnaddm1cl  9404  nn0n0n1ge2  9413  zdivadd  9432  zdivmul  9433  suprzclex  9441  zneo  9444  peano5uzti  9451  supinfneg  9686  infsupneg  9687  qmulz  9714  qnegcl  9727  qapne  9730  qdivcl  9734  cnref1o  9742  xnegcl  9924  xltnegi  9927  xaddnemnf  9949  xaddnepnf  9950  xnegdi  9960  xnpcan  9964  xltadd1  9968  xposdif  9974  xleaddadd  9979  iccf1o  10096  ige3m2fz  10141  ige2m1fz1  10201  zssinfcl  10339  infssuzex  10340  infssuzcldc  10342  zsupssdc  10345  suprzcl2dc  10346  rebtwn2z  10361  flqcl  10380  flapcl  10382  ceilqcl  10417  intfracq  10429  modqcl  10435  mulqmod0  10439  modqdifz  10445  zmodcl  10453  modfzo0difsn  10504  modsumfzodifsn  10505  frec2uzzd  10509  frec2uzsucd  10510  frec2uzuzd  10511  frecuzrdgrrn  10517  frec2uzrdg  10518  frecuzrdgrcl  10519  frecuzrdgsuc  10523  frecuzrdgrclt  10524  frecuzrdgg  10525  frecuzrdgsuctlem  10532  fzofig  10541  iseqovex  10567  seq3val  10569  seqvalcd  10570  seqf  10573  seqovcd  10576  seq3clss  10580  seq3caopr3  10600  iseqf1olemnab  10610  iseqf1olemqk  10616  iseqf1olemjpcl  10617  iseqf1olemqpcl  10618  iseqf1olemfvp  10619  seq3f1olemqsumkj  10620  seq3f1olemqsum  10622  seq3f1oleml  10625  seq3f1o  10626  seqf1oglem2a  10627  seqf1oglem1  10628  seqf1oglem2  10629  seq3distr  10641  ser0f  10643  ser3le  10646  exp3vallem  10649  exp3val  10650  exp1  10654  expcl2lemap  10660  m1expcl2  10670  expaddzap  10692  sqcl  10709  nnsqcl  10718  qsqcl  10720  zesq  10767  facp1  10839  faccl  10844  facdiv  10847  bcval  10858  bcrpcl  10862  bcp1n  10870  bcpasc  10875  permnn  10880  hashennn  10889  hashcl  10890  lencl  10956  wrdexg  10963  elovmpowrd  10993  shftlem  10998  ovshftex  11001  shftf  11012  seq3shft  11020  cjth  11028  imval  11032  recl  11035  imcl  11036  crre  11039  remim  11042  reim0b  11044  cvg1nlemcau  11166  uzin2  11169  resqrexlem1arp  11187  resqrexlemp1rp  11188  resqrexlemglsq  11204  resqrexlemga  11205  resqrtcl  11211  abscl  11233  absrpclap  11243  nn0abscl  11267  fzomaxdiflem  11294  fzomaxdif  11295  maxabslemab  11388  maxcl  11392  zmaxcl  11406  minmax  11412  mincl  11413  xrmaxcl  11434  xrmaxaddlem  11442  xrminmax  11447  xrmincl  11448  xrmineqinf  11451  xrminrpcl  11456  reccn2ap  11495  climaddc1  11511  climmulc2  11513  climsubc1  11514  climsubc2  11515  climle  11516  climlec2  11523  climcvg1nlem  11531  sumrbdclem  11559  fsum3cvg  11560  summodclem3  11562  summodclem2a  11563  zsumdc  11566  fsumgcl  11568  fsum3  11569  isumss  11573  fisumss  11574  isumss2  11575  fsum3cvg2  11576  fsum3ser  11579  fsumcl2lem  11580  fsumcllem  11581  fsumadd  11588  sumsnf  11591  fsumsplitsn  11592  isumcl  11607  isummulc2  11608  isumrecl  11611  isumge0  11612  isumadd  11613  fsum2dlemstep  11616  fisumcom2  11620  mptfzshft  11624  fsumrev  11625  fsummulc2  11630  iserabs  11657  isumshft  11672  isumsplit  11673  isum1p  11674  isumrpcl  11676  isumle  11677  isumlessdc  11678  trireciplem  11682  expcnvap0  11684  expcnvre  11685  expcnv  11686  explecnv  11687  geolim  11693  geolim2  11694  geo2lim  11698  cvgratnnlemsumlt  11710  cvgratz  11714  mertenslemub  11716  mertenslemi1  11717  mertenslem2  11718  mertensabs  11719  prodf1f  11725  prodfdivap  11729  prodrbdclem  11753  fproddccvg  11754  prodmodclem3  11757  prodmodclem2a  11758  zproddc  11761  fprodseq  11765  fprodntrivap  11766  prodssdc  11771  fprodmul  11773  prodsnf  11774  fprodsplitdc  11778  fprodunsn  11786  fprodcl2lem  11787  fprodcllem  11788  fprodabs  11798  fprodrev  11801  fprod2dlemstep  11804  fprodcom2fi  11808  fprodsplitsn  11815  efcllemp  11840  ef0lem  11842  efcvgfsum  11849  reefcl  11850  ege2le3  11853  efcj  11855  efaddlem  11856  eftlcvg  11869  eftlcl  11870  reeftlcl  11871  eftlub  11872  efsep  11873  effsumlt  11874  efgt1p2  11877  efgt1p  11878  reeff1  11882  tanclap  11891  resincl  11902  recoscl  11903  retanclap  11904  eirraplem  11959  dvdsval2  11972  fsumdvds  12024  sqoddm1div8z  12068  bitsinv1lem  12143  gcdval  12151  gcdn0cl  12154  gcddvds  12155  divgcdnnr  12168  uzwodc  12229  nn0seqcvgd  12234  ialgrlem1st  12235  ialgrlemconst  12236  algrf  12238  algrp1  12239  eucalgf  12248  eucalglt  12250  lcmval  12256  lcmcllem  12260  lcmgcdlem  12270  cncongr2  12297  sqrt2irrlem  12354  oddpwdclemxy  12362  oddpwdclemdc  12366  qden1elz  12398  phicl2  12407  phimullem  12418  eulerthlemth  12425  prmdiv  12428  odzcllem  12436  pythagtriplem8  12466  pythagtriplem9  12467  pcval  12490  pczcl  12492  pcqcl  12500  dvdsprmpweqle  12531  pcaddlem  12533  pcmptcl  12536  pcmpt  12537  pockthlem  12550  pockthg  12551  zgz  12567  gznegcl  12569  gzcjcl  12570  gzaddcl  12571  gzmulcl  12572  gzabssqcl  12575  4sqlem5  12576  4sqlem4a  12585  mul4sqlem  12587  mul4sq  12588  4sqlemafi  12589  4sqlemffi  12590  4sqleminfi  12591  4sqexercise1  12592  4sqlem16  12600  4sqlem17  12601  ennnfonelemjn  12644  ennnfonelemg  12645  ennnfonelemp1  12648  ctinfomlemom  12669  ctiunctlemfo  12681  nninfdclemcl  12690  nninfdclemf  12691  nninfdclemp1  12692  setsex  12735  strsetsid  12736  strslfv3  12749  ressex  12768  ressbas2d  12771  strressid  12774  tgvalex  12965  ptex  12966  prdsex  12971  prdsval  12975  imasex  13007  imasival  13008  imasbas  13009  imasplusg  13010  imasmulr  13011  imasaddfn  13019  imasaddval  13020  imasaddf  13021  imasmulfn  13022  imasmulval  13023  imasmulf  13024  qusval  13025  qusex  13027  qusaddvallemg  13035  qusaddflemg  13036  qusaddval  13037  qusaddf  13038  qusmulval  13039  qusmulf  13040  mgm1  13072  gsumress  13097  gsumprval  13101  prdsplusgsgrpcl  13116  prdsplusgcl  13148  prdsidlem  13149  pwsmnd  13152  mhmex  13164  subsubm  13185  0subm  13186  mhmeql  13194  gsumwsubmcl  13198  gsumfzcl  13201  grpsubval  13248  grplinv  13252  pwsgrp  13313  qusgrp2  13319  mulgval  13328  mulgex  13329  mulgfng  13330  mulg1  13335  mulgnnp1  13336  mulgnnsubcl  13340  mulgnn0subcl  13341  mulgsubcl  13342  mulgnndir  13357  subgex  13382  subgsubcl  13391  issubgrpd  13397  subsubg  13403  nsgconj  13412  0nsg  13420  triv1nsgd  13424  eqgex  13427  eqger  13430  eqgcpbl  13434  ghmex  13461  ghmpreima  13472  ghmnsgpreima  13475  conjnmz  13485  gsumfzsubmcl  13544  mgpex  13557  rngmgpf  13569  qusrng  13590  mgpf  13643  qusring2  13698  opprex  13705  opprrng  13709  opprring  13711  dvdsrex  13730  opprunitd  13742  dvrvald  13766  dvrcl  13767  unitdvcl  13768  invrpropdg  13781  subsubrng  13846  subrgcrng  13857  subrgsubm  13866  subrgugrp  13872  subsubrg  13877  rnrhmsubrg  13884  aprcotr  13917  rmodislmod  13983  lssvsubcl  13998  islss3  14011  lspex  14027  ellspsn  14049  sraex  14078  rlmlmod  14096  lidlex  14105  rspex  14106  lidl0cl  14115  lidlacl  14116  lidlnegcl  14117  ridl0  14142  ridl1  14143  2idlelbas  14148  cnsubglem  14211  expghmap  14239  mulgrhm  14241  zrhex  14253  znbaslemnn  14271  psrval  14296  psrbasg  14303  iunopn  14322  toponmax  14345  tgtop  14388  tgiun  14393  tgidm  14394  ntropn  14437  tgrest  14489  restopnb  14501  cnovex  14516  cnclima  14543  txvalex  14574  txtop  14580  tx1cn  14589  tx2cn  14590  txcnp  14591  txcnmpt  14593  txdis1cn  14598  cnmptcom  14618  imasnopn  14619  hmeocnv  14627  hmeores  14635  txhmeo  14639  txswaphmeo  14641  ispsmet  14643  xmetres  14702  metres  14703  blex  14707  xmeter  14756  xmetresbl  14760  mopntopon  14763  isxms2  14772  xmetxp  14827  xmettx  14830  txmetcnp  14838  qtopbasss  14841  qtopbas  14842  reopnap  14866  ioo2blex  14872  blssioo  14873  tgioo  14874  fsumcncntop  14887  expcn  14889  cncfval  14892  divccncfap  14910  cdivcncfap  14924  divcncfap  14934  maxcncf  14935  mincncf  14936  ivthdec  14964  hoverb  14968  limccnpcntop  14995  dvrecap  15033  elplyd  15061  ply1termlem  15062  ply1term  15063  plymullem1  15068  plyaddlem  15069  plymullem  15070  plycolemc  15078  plyco  15079  plycj  15081  plycn  15082  plyreres  15084  dvply1  15085  dvply2g  15086  pilem3  15103  tanrpcl  15157  cosordlem  15169  ioocosf1o  15174  rpcncxpcl  15222  rpcxpcl  15223  rpabscxpbnd  15260  rplogbcl  15266  sgmnncl  15308  mpodvdsmulf1o  15310  fsumdvdsmul  15311  mersenne  15317  perfectlem2  15320  lgslem1  15325  lgsval  15329  lgscllem  15332  lgsne0  15363  gausslemma2dlem4  15389  lgseisenlem1  15395  lgsquadlem1  15402  lgsquadlem2  15403  2sqlem3  15442  2sqlem8  15448  djucllem  15530  012of  15724  2o01f  15725  nninfsellemeq  15745  qdencn  15758  cvgcmp2nlemabs  15763  trilpolemclim  15767  trilpolemisumle  15769  trilpolemeq1  15771  trilpolemlt1  15772  nconstwlpolemgt0  15795