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  5643  fvmptdf  5650  fvmptt  5654  elfvmptrab  5658  dffo3  5710  resfunexg  5784  f1oiso2  5875  riota2df  5899  riota5f  5903  ovmpodxf  6049  ovmpodf  6055  offval  6144  ofvalg  6146  offeq  6150  iunexg  6177  oprabexd  6185  fo1stresm  6220  fo2ndresm  6221  oprssdmm  6230  1stdm  6241  1stconst  6280  2ndconst  6281  cnvf1olem  6283  fo2ndf  6286  f1od2  6294  iunon  6343  tfrlemibacc  6385  tfrlemibfn  6387  tfr1onlembacc  6401  tfr1onlembfn  6403  tfrcllembacc  6414  tfrcllembfn  6416  tfrcl  6423  rdgon  6445  frec0g  6456  freccllem  6461  frecfcllem  6463  frecsuclem  6465  oacl  6519  omcl  6520  oeicl  6521  nntr2  6562  mptelixpg  6794  fidifsnen  6932  en2eqpr  6969  unfiin  6988  tpfidceq  6992  ssfirab  6998  fnfi  7003  relcnvfi  7008  fidcenumlemr  7022  elfi2  7039  supclti  7065  supubti  7066  suplubti  7067  supelti  7069  ordiso2  7102  djulclr  7116  djurclr  7117  djulcl  7118  djurcl  7119  djuss  7137  updjudhcoinlf  7147  updjudhcoinrg  7148  ctssdclemn0  7177  ctssdccl  7178  ctssdc  7180  enumctlemm  7181  nninfwlpoimlemg  7242  cardcl  7249  exmidontriimlem2  7291  exmidapne  7329  cc2lem  7335  cc3  7337  addclpi  7396  mulclpi  7397  addclnq  7444  mulclnq  7445  addclnq0  7520  mulclnq0  7521  nqpnq0nq  7522  elnp1st2nd  7545  prarloclemcalc  7571  distrlem1prl  7651  distrlem1pru  7652  ltexprlemopl  7670  ltexprlemopu  7672  ltexprlemfl  7678  ltexprlemrl  7679  ltexprlemfu  7680  ltexprlemru  7681  addcanprlemu  7684  recexprlemloc  7700  aptiprleml  7708  caucvgprprlemopl  7766  suplocexprlemex  7791  addclsr  7822  mulclsr  7823  recexgt0sr  7842  mulextsr1lem  7849  suplocsrlemb  7875  suplocsrlempr  7876  suplocsrlem  7877  axaddcl  7933  axaddrcl  7934  axmulcl  7935  axmulrcl  7936  axcaucvglemval  7966  subcl  8227  cru  8631  aprcl  8675  aptap  8679  divclap  8707  redivclap  8760  diveqap1bd  8865  lbinfcl  8978  cju  8990  nn1m1nn  9010  nnsub  9031  nnnn0addcl  9281  un0addcl  9284  peano2z  9364  peano2zm  9366  zaddcllemneg  9367  zaddcl  9368  nnaddm1cl  9389  nn0n0n1ge2  9398  zdivadd  9417  zdivmul  9418  suprzclex  9426  zneo  9429  peano5uzti  9436  supinfneg  9671  infsupneg  9672  qmulz  9699  qnegcl  9712  qapne  9715  qdivcl  9719  cnref1o  9727  xnegcl  9909  xltnegi  9912  xaddnemnf  9934  xaddnepnf  9935  xnegdi  9945  xnpcan  9949  xltadd1  9953  xposdif  9959  xleaddadd  9964  iccf1o  10081  ige3m2fz  10126  ige2m1fz1  10186  zssinfcl  10324  infssuzex  10325  infssuzcldc  10327  zsupssdc  10330  suprzcl2dc  10331  rebtwn2z  10346  flqcl  10365  flapcl  10367  ceilqcl  10402  intfracq  10414  modqcl  10420  mulqmod0  10424  modqdifz  10430  zmodcl  10438  modfzo0difsn  10489  modsumfzodifsn  10490  frec2uzzd  10494  frec2uzsucd  10495  frec2uzuzd  10496  frecuzrdgrrn  10502  frec2uzrdg  10503  frecuzrdgrcl  10504  frecuzrdgsuc  10508  frecuzrdgrclt  10509  frecuzrdgg  10510  frecuzrdgsuctlem  10517  fzofig  10526  iseqovex  10552  seq3val  10554  seqvalcd  10555  seqf  10558  seqovcd  10561  seq3clss  10565  seq3caopr3  10585  iseqf1olemnab  10595  iseqf1olemqk  10601  iseqf1olemjpcl  10602  iseqf1olemqpcl  10603  iseqf1olemfvp  10604  seq3f1olemqsumkj  10605  seq3f1olemqsum  10607  seq3f1oleml  10610  seq3f1o  10611  seqf1oglem2a  10612  seqf1oglem1  10613  seqf1oglem2  10614  seq3distr  10626  ser0f  10628  ser3le  10631  exp3vallem  10634  exp3val  10635  exp1  10639  expcl2lemap  10645  m1expcl2  10655  expaddzap  10677  sqcl  10694  nnsqcl  10703  qsqcl  10705  zesq  10752  facp1  10824  faccl  10829  facdiv  10832  bcval  10843  bcrpcl  10847  bcp1n  10855  bcpasc  10860  permnn  10865  hashennn  10874  hashcl  10875  lencl  10941  wrdexg  10948  elovmpowrd  10978  shftlem  10983  ovshftex  10986  shftf  10997  seq3shft  11005  cjth  11013  imval  11017  recl  11020  imcl  11021  crre  11024  remim  11027  reim0b  11029  cvg1nlemcau  11151  uzin2  11154  resqrexlem1arp  11172  resqrexlemp1rp  11173  resqrexlemglsq  11189  resqrexlemga  11190  resqrtcl  11196  abscl  11218  absrpclap  11228  nn0abscl  11252  fzomaxdiflem  11279  fzomaxdif  11280  maxabslemab  11373  maxcl  11377  zmaxcl  11391  minmax  11397  mincl  11398  xrmaxcl  11419  xrmaxaddlem  11427  xrminmax  11432  xrmincl  11433  xrmineqinf  11436  xrminrpcl  11441  reccn2ap  11480  climaddc1  11496  climmulc2  11498  climsubc1  11499  climsubc2  11500  climle  11501  climlec2  11508  climcvg1nlem  11516  sumrbdclem  11544  fsum3cvg  11545  summodclem3  11547  summodclem2a  11548  zsumdc  11551  fsumgcl  11553  fsum3  11554  isumss  11558  fisumss  11559  isumss2  11560  fsum3cvg2  11561  fsum3ser  11564  fsumcl2lem  11565  fsumcllem  11566  fsumadd  11573  sumsnf  11576  fsumsplitsn  11577  isumcl  11592  isummulc2  11593  isumrecl  11596  isumge0  11597  isumadd  11598  fsum2dlemstep  11601  fisumcom2  11605  mptfzshft  11609  fsumrev  11610  fsummulc2  11615  iserabs  11642  isumshft  11657  isumsplit  11658  isum1p  11659  isumrpcl  11661  isumle  11662  isumlessdc  11663  trireciplem  11667  expcnvap0  11669  expcnvre  11670  expcnv  11671  explecnv  11672  geolim  11678  geolim2  11679  geo2lim  11683  cvgratnnlemsumlt  11695  cvgratz  11699  mertenslemub  11701  mertenslemi1  11702  mertenslem2  11703  mertensabs  11704  prodf1f  11710  prodfdivap  11714  prodrbdclem  11738  fproddccvg  11739  prodmodclem3  11742  prodmodclem2a  11743  zproddc  11746  fprodseq  11750  fprodntrivap  11751  prodssdc  11756  fprodmul  11758  prodsnf  11759  fprodsplitdc  11763  fprodunsn  11771  fprodcl2lem  11772  fprodcllem  11773  fprodabs  11783  fprodrev  11786  fprod2dlemstep  11789  fprodcom2fi  11793  fprodsplitsn  11800  efcllemp  11825  ef0lem  11827  efcvgfsum  11834  reefcl  11835  ege2le3  11838  efcj  11840  efaddlem  11841  eftlcvg  11854  eftlcl  11855  reeftlcl  11856  eftlub  11857  efsep  11858  effsumlt  11859  efgt1p2  11862  efgt1p  11863  reeff1  11867  tanclap  11876  resincl  11887  recoscl  11888  retanclap  11889  eirraplem  11944  dvdsval2  11957  fsumdvds  12009  sqoddm1div8z  12053  bitsinv1lem  12128  gcdval  12136  gcdn0cl  12139  gcddvds  12140  divgcdnnr  12153  uzwodc  12214  nn0seqcvgd  12219  ialgrlem1st  12220  ialgrlemconst  12221  algrf  12223  algrp1  12224  eucalgf  12233  eucalglt  12235  lcmval  12241  lcmcllem  12245  lcmgcdlem  12255  cncongr2  12282  sqrt2irrlem  12339  oddpwdclemxy  12347  oddpwdclemdc  12351  qden1elz  12383  phicl2  12392  phimullem  12403  eulerthlemth  12410  prmdiv  12413  odzcllem  12421  pythagtriplem8  12451  pythagtriplem9  12452  pcval  12475  pczcl  12477  pcqcl  12485  dvdsprmpweqle  12516  pcaddlem  12518  pcmptcl  12521  pcmpt  12522  pockthlem  12535  pockthg  12536  zgz  12552  gznegcl  12554  gzcjcl  12555  gzaddcl  12556  gzmulcl  12557  gzabssqcl  12560  4sqlem5  12561  4sqlem4a  12570  mul4sqlem  12572  mul4sq  12573  4sqlemafi  12574  4sqlemffi  12575  4sqleminfi  12576  4sqexercise1  12577  4sqlem16  12585  4sqlem17  12586  ennnfonelemjn  12629  ennnfonelemg  12630  ennnfonelemp1  12633  ctinfomlemom  12654  ctiunctlemfo  12666  nninfdclemcl  12675  nninfdclemf  12676  nninfdclemp1  12677  setsex  12720  strsetsid  12721  ressex  12753  ressbas2d  12756  strressid  12759  tgvalex  12944  ptex  12945  prdsex  12950  imasex  12958  imasival  12959  imasbas  12960  imasplusg  12961  imasmulr  12962  imasaddfn  12970  imasaddval  12971  imasaddf  12972  imasmulfn  12973  imasmulval  12974  imasmulf  12975  qusval  12976  qusex  12978  qusaddvallemg  12986  qusaddflemg  12987  qusaddval  12988  qusaddf  12989  qusmulval  12990  qusmulf  12991  mgm1  13023  gsumress  13048  gsumprval  13052  mhmex  13104  subsubm  13125  0subm  13126  mhmeql  13134  gsumwsubmcl  13138  gsumfzcl  13141  grpsubval  13188  grplinv  13192  qusgrp2  13253  mulgval  13262  mulgex  13263  mulgfng  13264  mulg1  13269  mulgnnp1  13270  mulgnnsubcl  13274  mulgnn0subcl  13275  mulgsubcl  13276  mulgnndir  13291  subgex  13316  subgsubcl  13325  issubgrpd  13331  subsubg  13337  nsgconj  13346  0nsg  13354  triv1nsgd  13358  eqgex  13361  eqger  13364  eqgcpbl  13368  ghmex  13395  ghmpreima  13406  ghmnsgpreima  13409  conjnmz  13419  gsumfzsubmcl  13478  mgpex  13491  rngmgpf  13503  qusrng  13524  mgpf  13577  qusring2  13632  opprex  13639  opprrng  13643  opprring  13645  dvdsrex  13664  opprunitd  13676  dvrvald  13700  dvrcl  13701  unitdvcl  13702  invrpropdg  13715  subsubrng  13780  subrgcrng  13791  subrgsubm  13800  subrgugrp  13806  subsubrg  13811  rnrhmsubrg  13818  aprcotr  13851  rmodislmod  13917  lssvsubcl  13932  islss3  13945  lspex  13961  ellspsn  13983  sraex  14012  rlmlmod  14030  lidlex  14039  rspex  14040  lidl0cl  14049  lidlacl  14050  lidlnegcl  14051  ridl0  14076  ridl1  14077  2idlelbas  14082  cnsubglem  14145  expghmap  14173  mulgrhm  14175  zrhex  14187  znbaslemnn  14205  psrval  14230  psrbasg  14237  iunopn  14248  toponmax  14271  tgtop  14314  tgiun  14319  tgidm  14320  ntropn  14363  tgrest  14415  restopnb  14427  cnovex  14442  cnclima  14469  txvalex  14500  txtop  14506  tx1cn  14515  tx2cn  14516  txcnp  14517  txcnmpt  14519  txdis1cn  14524  cnmptcom  14544  imasnopn  14545  hmeocnv  14553  hmeores  14561  txhmeo  14565  txswaphmeo  14567  ispsmet  14569  xmetres  14628  metres  14629  blex  14633  xmeter  14682  xmetresbl  14686  mopntopon  14689  isxms2  14698  xmetxp  14753  xmettx  14756  txmetcnp  14764  qtopbasss  14767  qtopbas  14768  reopnap  14792  ioo2blex  14798  blssioo  14799  tgioo  14800  fsumcncntop  14813  expcn  14815  cncfval  14818  divccncfap  14836  cdivcncfap  14850  divcncfap  14860  maxcncf  14861  mincncf  14862  ivthdec  14890  hoverb  14894  limccnpcntop  14921  dvrecap  14959  elplyd  14987  ply1termlem  14988  ply1term  14989  plymullem1  14994  plyaddlem  14995  plymullem  14996  plycolemc  15004  plyco  15005  plycj  15007  plycn  15008  plyreres  15010  dvply1  15011  dvply2g  15012  pilem3  15029  tanrpcl  15083  cosordlem  15095  ioocosf1o  15100  rpcncxpcl  15148  rpcxpcl  15149  rpabscxpbnd  15186  rplogbcl  15192  sgmnncl  15234  mpodvdsmulf1o  15236  fsumdvdsmul  15237  mersenne  15243  perfectlem2  15246  lgslem1  15251  lgsval  15255  lgscllem  15258  lgsne0  15289  gausslemma2dlem4  15315  lgseisenlem1  15321  lgsquadlem1  15328  lgsquadlem2  15329  2sqlem3  15368  2sqlem8  15374  djucllem  15456  012of  15650  2o01f  15651  nninfsellemeq  15668  qdencn  15681  cvgcmp2nlemabs  15686  trilpolemclim  15690  trilpolemisumle  15692  trilpolemeq1  15694  trilpolemlt1  15695  nconstwlpolemgt0  15718