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  3590  ifcldcd  3597  intab  3903  disjiun  4028  iinexgm  4187  opexg  4261  tfisi  4623  nnpredcl  4659  imain  5340  fvmptd  5642  fvmptdf  5649  fvmptt  5653  elfvmptrab  5657  dffo3  5709  resfunexg  5783  f1oiso2  5874  riota2df  5898  riota5f  5902  ovmpodxf  6048  ovmpodf  6054  offval  6143  ofvalg  6145  offeq  6149  iunexg  6176  oprabexd  6184  fo1stresm  6219  fo2ndresm  6220  oprssdmm  6229  1stdm  6240  1stconst  6279  2ndconst  6280  cnvf1olem  6282  fo2ndf  6285  f1od2  6293  iunon  6342  tfrlemibacc  6384  tfrlemibfn  6386  tfr1onlembacc  6400  tfr1onlembfn  6402  tfrcllembacc  6413  tfrcllembfn  6415  tfrcl  6422  rdgon  6444  frec0g  6455  freccllem  6460  frecfcllem  6462  frecsuclem  6464  oacl  6518  omcl  6519  oeicl  6520  nntr2  6561  mptelixpg  6793  fidifsnen  6931  en2eqpr  6968  unfiin  6987  tpfidceq  6991  ssfirab  6997  fnfi  7002  relcnvfi  7007  fidcenumlemr  7021  elfi2  7038  supclti  7064  supubti  7065  suplubti  7066  supelti  7068  ordiso2  7101  djulclr  7115  djurclr  7116  djulcl  7117  djurcl  7118  djuss  7136  updjudhcoinlf  7146  updjudhcoinrg  7147  ctssdclemn0  7176  ctssdccl  7177  ctssdc  7179  enumctlemm  7180  nninfwlpoimlemg  7241  cardcl  7248  exmidontriimlem2  7289  exmidapne  7327  cc2lem  7333  cc3  7335  addclpi  7394  mulclpi  7395  addclnq  7442  mulclnq  7443  addclnq0  7518  mulclnq0  7519  nqpnq0nq  7520  elnp1st2nd  7543  prarloclemcalc  7569  distrlem1prl  7649  distrlem1pru  7650  ltexprlemopl  7668  ltexprlemopu  7670  ltexprlemfl  7676  ltexprlemrl  7677  ltexprlemfu  7678  ltexprlemru  7679  addcanprlemu  7682  recexprlemloc  7698  aptiprleml  7706  caucvgprprlemopl  7764  suplocexprlemex  7789  addclsr  7820  mulclsr  7821  recexgt0sr  7840  mulextsr1lem  7847  suplocsrlemb  7873  suplocsrlempr  7874  suplocsrlem  7875  axaddcl  7931  axaddrcl  7932  axmulcl  7933  axmulrcl  7934  axcaucvglemval  7964  subcl  8225  cru  8629  aprcl  8673  aptap  8677  divclap  8705  redivclap  8758  diveqap1bd  8863  lbinfcl  8976  cju  8988  nn1m1nn  9008  nnsub  9029  nnnn0addcl  9279  un0addcl  9282  peano2z  9362  peano2zm  9364  zaddcllemneg  9365  zaddcl  9366  nnaddm1cl  9387  nn0n0n1ge2  9396  zdivadd  9415  zdivmul  9416  suprzclex  9424  zneo  9427  peano5uzti  9434  supinfneg  9669  infsupneg  9670  qmulz  9697  qnegcl  9710  qapne  9713  qdivcl  9717  cnref1o  9725  xnegcl  9907  xltnegi  9910  xaddnemnf  9932  xaddnepnf  9933  xnegdi  9943  xnpcan  9947  xltadd1  9951  xposdif  9957  xleaddadd  9962  iccf1o  10079  ige3m2fz  10124  ige2m1fz1  10184  zssinfcl  10322  infssuzex  10323  infssuzcldc  10325  zsupssdc  10328  suprzcl2dc  10329  rebtwn2z  10344  flqcl  10363  flapcl  10365  ceilqcl  10400  intfracq  10412  modqcl  10418  mulqmod0  10422  modqdifz  10428  zmodcl  10436  modfzo0difsn  10487  modsumfzodifsn  10488  frec2uzzd  10492  frec2uzsucd  10493  frec2uzuzd  10494  frecuzrdgrrn  10500  frec2uzrdg  10501  frecuzrdgrcl  10502  frecuzrdgsuc  10506  frecuzrdgrclt  10507  frecuzrdgg  10508  frecuzrdgsuctlem  10515  fzofig  10524  iseqovex  10550  seq3val  10552  seqvalcd  10553  seqf  10556  seqovcd  10559  seq3clss  10563  seq3caopr3  10583  iseqf1olemnab  10593  iseqf1olemqk  10599  iseqf1olemjpcl  10600  iseqf1olemqpcl  10601  iseqf1olemfvp  10602  seq3f1olemqsumkj  10603  seq3f1olemqsum  10605  seq3f1oleml  10608  seq3f1o  10609  seqf1oglem2a  10610  seqf1oglem1  10611  seqf1oglem2  10612  seq3distr  10624  ser0f  10626  ser3le  10629  exp3vallem  10632  exp3val  10633  exp1  10637  expcl2lemap  10643  m1expcl2  10653  expaddzap  10675  sqcl  10692  nnsqcl  10701  qsqcl  10703  zesq  10750  facp1  10822  faccl  10827  facdiv  10830  bcval  10841  bcrpcl  10845  bcp1n  10853  bcpasc  10858  permnn  10863  hashennn  10872  hashcl  10873  lencl  10939  wrdexg  10946  elovmpowrd  10976  shftlem  10981  ovshftex  10984  shftf  10995  seq3shft  11003  cjth  11011  imval  11015  recl  11018  imcl  11019  crre  11022  remim  11025  reim0b  11027  cvg1nlemcau  11149  uzin2  11152  resqrexlem1arp  11170  resqrexlemp1rp  11171  resqrexlemglsq  11187  resqrexlemga  11188  resqrtcl  11194  abscl  11216  absrpclap  11226  nn0abscl  11250  fzomaxdiflem  11277  fzomaxdif  11278  maxabslemab  11371  maxcl  11375  zmaxcl  11389  minmax  11395  mincl  11396  xrmaxcl  11417  xrmaxaddlem  11425  xrminmax  11430  xrmincl  11431  xrmineqinf  11434  xrminrpcl  11439  reccn2ap  11478  climaddc1  11494  climmulc2  11496  climsubc1  11497  climsubc2  11498  climle  11499  climlec2  11506  climcvg1nlem  11514  sumrbdclem  11542  fsum3cvg  11543  summodclem3  11545  summodclem2a  11546  zsumdc  11549  fsumgcl  11551  fsum3  11552  isumss  11556  fisumss  11557  isumss2  11558  fsum3cvg2  11559  fsum3ser  11562  fsumcl2lem  11563  fsumcllem  11564  fsumadd  11571  sumsnf  11574  fsumsplitsn  11575  isumcl  11590  isummulc2  11591  isumrecl  11594  isumge0  11595  isumadd  11596  fsum2dlemstep  11599  fisumcom2  11603  mptfzshft  11607  fsumrev  11608  fsummulc2  11613  iserabs  11640  isumshft  11655  isumsplit  11656  isum1p  11657  isumrpcl  11659  isumle  11660  isumlessdc  11661  trireciplem  11665  expcnvap0  11667  expcnvre  11668  expcnv  11669  explecnv  11670  geolim  11676  geolim2  11677  geo2lim  11681  cvgratnnlemsumlt  11693  cvgratz  11697  mertenslemub  11699  mertenslemi1  11700  mertenslem2  11701  mertensabs  11702  prodf1f  11708  prodfdivap  11712  prodrbdclem  11736  fproddccvg  11737  prodmodclem3  11740  prodmodclem2a  11741  zproddc  11744  fprodseq  11748  fprodntrivap  11749  prodssdc  11754  fprodmul  11756  prodsnf  11757  fprodsplitdc  11761  fprodunsn  11769  fprodcl2lem  11770  fprodcllem  11771  fprodabs  11781  fprodrev  11784  fprod2dlemstep  11787  fprodcom2fi  11791  fprodsplitsn  11798  efcllemp  11823  ef0lem  11825  efcvgfsum  11832  reefcl  11833  ege2le3  11836  efcj  11838  efaddlem  11839  eftlcvg  11852  eftlcl  11853  reeftlcl  11854  eftlub  11855  efsep  11856  effsumlt  11857  efgt1p2  11860  efgt1p  11861  reeff1  11865  tanclap  11874  resincl  11885  recoscl  11886  retanclap  11887  eirraplem  11942  dvdsval2  11955  fsumdvds  12007  sqoddm1div8z  12051  gcdval  12126  gcdn0cl  12129  gcddvds  12130  divgcdnnr  12143  uzwodc  12204  nn0seqcvgd  12209  ialgrlem1st  12210  ialgrlemconst  12211  algrf  12213  algrp1  12214  eucalgf  12223  eucalglt  12225  lcmval  12231  lcmcllem  12235  lcmgcdlem  12245  cncongr2  12272  sqrt2irrlem  12329  oddpwdclemxy  12337  oddpwdclemdc  12341  qden1elz  12373  phicl2  12382  phimullem  12393  eulerthlemth  12400  prmdiv  12403  odzcllem  12411  pythagtriplem8  12441  pythagtriplem9  12442  pcval  12465  pczcl  12467  pcqcl  12475  dvdsprmpweqle  12506  pcaddlem  12508  pcmptcl  12511  pcmpt  12512  pockthlem  12525  pockthg  12526  zgz  12542  gznegcl  12544  gzcjcl  12545  gzaddcl  12546  gzmulcl  12547  gzabssqcl  12550  4sqlem5  12551  4sqlem4a  12560  mul4sqlem  12562  mul4sq  12563  4sqlemafi  12564  4sqlemffi  12565  4sqleminfi  12566  4sqexercise1  12567  4sqlem16  12575  4sqlem17  12576  ennnfonelemjn  12619  ennnfonelemg  12620  ennnfonelemp1  12623  ctinfomlemom  12644  ctiunctlemfo  12656  nninfdclemcl  12665  nninfdclemf  12666  nninfdclemp1  12667  setsex  12710  strsetsid  12711  ressex  12743  ressbas2d  12746  strressid  12749  tgvalex  12934  ptex  12935  prdsex  12940  imasex  12948  imasival  12949  imasbas  12950  imasplusg  12951  imasmulr  12952  imasaddfn  12960  imasaddval  12961  imasaddf  12962  imasmulfn  12963  imasmulval  12964  imasmulf  12965  qusval  12966  qusex  12968  qusaddvallemg  12976  qusaddflemg  12977  qusaddval  12978  qusaddf  12979  qusmulval  12980  qusmulf  12981  mgm1  13013  gsumress  13038  gsumprval  13042  mhmex  13094  subsubm  13115  0subm  13116  mhmeql  13124  gsumwsubmcl  13128  gsumfzcl  13131  grpsubval  13178  grplinv  13182  qusgrp2  13243  mulgval  13252  mulgex  13253  mulgfng  13254  mulg1  13259  mulgnnp1  13260  mulgnnsubcl  13264  mulgnn0subcl  13265  mulgsubcl  13266  mulgnndir  13281  subgex  13306  subgsubcl  13315  issubgrpd  13321  subsubg  13327  nsgconj  13336  0nsg  13344  triv1nsgd  13348  eqgex  13351  eqger  13354  eqgcpbl  13358  ghmex  13385  ghmpreima  13396  ghmnsgpreima  13399  conjnmz  13409  gsumfzsubmcl  13468  mgpex  13481  rngmgpf  13493  qusrng  13514  mgpf  13567  qusring2  13622  opprex  13629  opprrng  13633  opprring  13635  dvdsrex  13654  opprunitd  13666  dvrvald  13690  dvrcl  13691  unitdvcl  13692  invrpropdg  13705  subsubrng  13770  subrgcrng  13781  subrgsubm  13790  subrgugrp  13796  subsubrg  13801  rnrhmsubrg  13808  aprcotr  13841  rmodislmod  13907  lssvsubcl  13922  islss3  13935  lspex  13951  ellspsn  13973  sraex  14002  rlmlmod  14020  lidlex  14029  rspex  14030  lidl0cl  14039  lidlacl  14040  lidlnegcl  14041  ridl0  14066  ridl1  14067  2idlelbas  14072  cnsubglem  14135  expghmap  14163  mulgrhm  14165  zrhex  14177  znbaslemnn  14195  psrval  14220  psrbasg  14227  iunopn  14238  toponmax  14261  tgtop  14304  tgiun  14309  tgidm  14310  ntropn  14353  tgrest  14405  restopnb  14417  cnovex  14432  cnclima  14459  txvalex  14490  txtop  14496  tx1cn  14505  tx2cn  14506  txcnp  14507  txcnmpt  14509  txdis1cn  14514  cnmptcom  14534  imasnopn  14535  hmeocnv  14543  hmeores  14551  txhmeo  14555  txswaphmeo  14557  ispsmet  14559  xmetres  14618  metres  14619  blex  14623  xmeter  14672  xmetresbl  14676  mopntopon  14679  isxms2  14688  xmetxp  14743  xmettx  14746  txmetcnp  14754  qtopbasss  14757  qtopbas  14758  reopnap  14782  ioo2blex  14788  blssioo  14789  tgioo  14790  fsumcncntop  14803  expcn  14805  cncfval  14808  divccncfap  14826  cdivcncfap  14840  divcncfap  14850  maxcncf  14851  mincncf  14852  ivthdec  14880  hoverb  14884  limccnpcntop  14911  dvrecap  14949  elplyd  14977  ply1termlem  14978  ply1term  14979  plymullem1  14984  plyaddlem  14985  plymullem  14986  plycolemc  14994  plyco  14995  plycj  14997  plycn  14998  plyreres  15000  dvply1  15001  dvply2g  15002  pilem3  15019  tanrpcl  15073  cosordlem  15085  ioocosf1o  15090  rpcncxpcl  15138  rpcxpcl  15139  rpabscxpbnd  15176  rplogbcl  15182  sgmnncl  15224  mpodvdsmulf1o  15226  fsumdvdsmul  15227  mersenne  15233  perfectlem2  15236  lgslem1  15241  lgsval  15245  lgscllem  15248  lgsne0  15279  gausslemma2dlem4  15305  lgseisenlem1  15311  lgsquadlem1  15318  lgsquadlem2  15319  2sqlem3  15358  2sqlem8  15364  djucllem  15446  012of  15640  2o01f  15641  nninfsellemeq  15658  qdencn  15671  cvgcmp2nlemabs  15676  trilpolemclim  15680  trilpolemisumle  15682  trilpolemeq1  15684  trilpolemlt1  15685  nconstwlpolemgt0  15708