Theorem eqeltrd 2254

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

Syntax hints:   -> wi 4   = wceq 1353   e. wcel 2148

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  eqeltrrd  2255  3eltr4d  2261  eqeltrid  2264  eqeltrdi  2268  ifcldadc  3564  ifcldcd  3571  intab  3874  disjiun  3999  iinexgm  4155  opexg  4229  tfisi  4587  nnpredcl  4623  imain  5299  fvmptd  5598  fvmptdf  5604  fvmptt  5608  elfvmptrab  5612  dffo3  5664  resfunexg  5738  f1oiso2  5828  riota2df  5851  riota5f  5855  ovmpodxf  6000  ovmpodf  6006  offval  6090  ofvalg  6092  offeq  6096  iunexg  6120  oprabexd  6128  fo1stresm  6162  fo2ndresm  6163  oprssdmm  6172  1stdm  6183  1stconst  6222  2ndconst  6223  cnvf1olem  6225  fo2ndf  6228  f1od2  6236  iunon  6285  tfrlemibacc  6327  tfrlemibfn  6329  tfr1onlembacc  6343  tfr1onlembfn  6345  tfrcllembacc  6356  tfrcllembfn  6358  tfrcl  6365  rdgon  6387  frec0g  6398  freccllem  6403  frecfcllem  6405  frecsuclem  6407  oacl  6461  omcl  6462  oeicl  6463  nntr2  6504  mptelixpg  6734  fidifsnen  6870  en2eqpr  6907  unfiin  6925  ssfirab  6933  fnfi  6936  relcnvfi  6940  fidcenumlemr  6954  elfi2  6971  supclti  6997  supubti  6998  suplubti  6999  supelti  7001  ordiso2  7034  djulclr  7048  djurclr  7049  djulcl  7050  djurcl  7051  djuss  7069  updjudhcoinlf  7079  updjudhcoinrg  7080  ctssdclemn0  7109  ctssdccl  7110  ctssdc  7112  enumctlemm  7113  nninfwlpoimlemg  7173  cardcl  7180  exmidontriimlem2  7221  exmidapne  7259  cc2lem  7265  cc3  7267  addclpi  7326  mulclpi  7327  addclnq  7374  mulclnq  7375  addclnq0  7450  mulclnq0  7451  nqpnq0nq  7452  elnp1st2nd  7475  prarloclemcalc  7501  distrlem1prl  7581  distrlem1pru  7582  ltexprlemopl  7600  ltexprlemopu  7602  ltexprlemfl  7608  ltexprlemrl  7609  ltexprlemfu  7610  ltexprlemru  7611  addcanprlemu  7614  recexprlemloc  7630  aptiprleml  7638  caucvgprprlemopl  7696  suplocexprlemex  7721  addclsr  7752  mulclsr  7753  recexgt0sr  7772  mulextsr1lem  7779  suplocsrlemb  7805  suplocsrlempr  7806  suplocsrlem  7807  axaddcl  7863  axaddrcl  7864  axmulcl  7865  axmulrcl  7866  axcaucvglemval  7896  subcl  8156  cru  8559  aprcl  8603  aptap  8607  divclap  8635  redivclap  8688  diveqap1bd  8793  lbinfcl  8906  cju  8918  nn1m1nn  8937  nnsub  8958  nnnn0addcl  9206  un0addcl  9209  peano2z  9289  peano2zm  9291  zaddcllemneg  9292  zaddcl  9293  nnaddm1cl  9314  nn0n0n1ge2  9323  zdivadd  9342  zdivmul  9343  suprzclex  9351  zneo  9354  peano5uzti  9361  supinfneg  9595  infsupneg  9596  qmulz  9623  qnegcl  9636  qapne  9639  qdivcl  9643  cnref1o  9650  xnegcl  9832  xltnegi  9835  xaddnemnf  9857  xaddnepnf  9858  xnegdi  9868  xnpcan  9872  xltadd1  9876  xposdif  9882  xleaddadd  9887  iccf1o  10004  ige3m2fz  10049  ige2m1fz1  10109  rebtwn2z  10255  flqcl  10273  flapcl  10275  ceilqcl  10308  intfracq  10320  modqcl  10326  mulqmod0  10330  modqdifz  10336  zmodcl  10344  modfzo0difsn  10395  modsumfzodifsn  10396  frec2uzzd  10400  frec2uzsucd  10401  frec2uzuzd  10402  frecuzrdgrrn  10408  frec2uzrdg  10409  frecuzrdgrcl  10410  frecuzrdgsuc  10414  frecuzrdgrclt  10415  frecuzrdgg  10416  frecuzrdgsuctlem  10423  fzofig  10432  iseqovex  10456  seq3val  10458  seqvalcd  10459  seqf  10461  seqovcd  10463  seq3clss  10467  seq3caopr3  10481  iseqf1olemnab  10488  iseqf1olemqk  10494  iseqf1olemjpcl  10495  iseqf1olemqpcl  10496  iseqf1olemfvp  10497  seq3f1olemqsumkj  10498  seq3f1olemqsum  10500  seq3f1oleml  10503  seq3f1o  10504  seq3distr  10513  ser0f  10515  ser3le  10518  exp3vallem  10521  exp3val  10522  exp1  10526  expcl2lemap  10532  m1expcl2  10542  expaddzap  10564  sqcl  10581  nnsqcl  10590  qsqcl  10592  zesq  10639  facp1  10710  faccl  10715  facdiv  10718  bcval  10729  bcrpcl  10733  bcp1n  10741  bcpasc  10746  permnn  10751  hashennn  10760  hashcl  10761  shftlem  10825  ovshftex  10828  shftf  10839  seq3shft  10847  cjth  10855  imval  10859  recl  10862  imcl  10863  crre  10866  remim  10869  reim0b  10871  cvg1nlemcau  10993  uzin2  10996  resqrexlem1arp  11014  resqrexlemp1rp  11015  resqrexlemglsq  11031  resqrexlemga  11032  resqrtcl  11038  abscl  11060  absrpclap  11070  nn0abscl  11094  fzomaxdiflem  11121  fzomaxdif  11122  maxabslemab  11215  maxcl  11219  zmaxcl  11233  minmax  11238  mincl  11239  xrmaxcl  11260  xrmaxaddlem  11268  xrminmax  11273  xrmincl  11274  xrmineqinf  11277  xrminrpcl  11282  reccn2ap  11321  climaddc1  11337  climmulc2  11339  climsubc1  11340  climsubc2  11341  climle  11342  climlec2  11349  climcvg1nlem  11357  sumrbdclem  11385  fsum3cvg  11386  summodclem3  11388  summodclem2a  11389  zsumdc  11392  fsumgcl  11394  fsum3  11395  isumss  11399  fisumss  11400  isumss2  11401  fsum3cvg2  11402  fsum3ser  11405  fsumcl2lem  11406  fsumcllem  11407  fsumadd  11414  sumsnf  11417  fsumsplitsn  11418  isumcl  11433  isummulc2  11434  isumrecl  11437  isumge0  11438  isumadd  11439  fsum2dlemstep  11442  fisumcom2  11446  mptfzshft  11450  fsumrev  11451  fsummulc2  11456  iserabs  11483  isumshft  11498  isumsplit  11499  isum1p  11500  isumrpcl  11502  isumle  11503  isumlessdc  11504  trireciplem  11508  expcnvap0  11510  expcnvre  11511  expcnv  11512  explecnv  11513  geolim  11519  geolim2  11520  geo2lim  11524  cvgratnnlemsumlt  11536  cvgratz  11540  mertenslemub  11542  mertenslemi1  11543  mertenslem2  11544  mertensabs  11545  prodf1f  11551  prodfdivap  11555  prodrbdclem  11579  fproddccvg  11580  prodmodclem3  11583  prodmodclem2a  11584  zproddc  11587  fprodseq  11591  fprodntrivap  11592  prodssdc  11597  fprodmul  11599  prodsnf  11600  fprodsplitdc  11604  fprodunsn  11612  fprodcl2lem  11613  fprodcllem  11614  fprodabs  11624  fprodrev  11627  fprod2dlemstep  11630  fprodcom2fi  11634  fprodsplitsn  11641  efcllemp  11666  ef0lem  11668  efcvgfsum  11675  reefcl  11676  ege2le3  11679  efcj  11681  efaddlem  11682  eftlcvg  11695  eftlcl  11696  reeftlcl  11697  eftlub  11698  efsep  11699  effsumlt  11700  efgt1p2  11703  efgt1p  11704  reeff1  11708  tanclap  11717  resincl  11728  recoscl  11729  retanclap  11730  eirraplem  11784  dvdsval2  11797  sqoddm1div8z  11891  zssinfcl  11949  infssuzex  11950  infssuzcldc  11952  zsupssdc  11955  suprzcl2dc  11956  gcdval  11960  gcdn0cl  11963  gcddvds  11964  divgcdnnr  11977  uzwodc  12038  nn0seqcvgd  12041  ialgrlem1st  12042  ialgrlemconst  12043  algrf  12045  algrp1  12046  eucalgf  12055  eucalglt  12057  lcmval  12063  lcmcllem  12067  lcmgcdlem  12077  cncongr2  12104  sqrt2irrlem  12161  oddpwdclemxy  12169  oddpwdclemdc  12173  qden1elz  12205  phicl2  12214  phimullem  12225  eulerthlemth  12232  prmdiv  12235  odzcllem  12242  pythagtriplem8  12272  pythagtriplem9  12273  pcval  12296  pczcl  12298  pcqcl  12306  dvdsprmpweqle  12336  pcaddlem  12338  pcmptcl  12340  pcmpt  12341  pockthlem  12354  pockthg  12355  zgz  12371  gznegcl  12373  gzcjcl  12374  gzaddcl  12375  gzmulcl  12376  gzabssqcl  12379  4sqlem5  12380  4sqlem4a  12389  mul4sqlem  12391  mul4sq  12392  ennnfonelemjn  12403  ennnfonelemg  12404  ennnfonelemp1  12407  ctinfomlemom  12428  ctiunctlemfo  12440  nninfdclemcl  12449  nninfdclemf  12450  nninfdclemp1  12451  setsex  12494  strsetsid  12495  ressex  12525  ressbas2d  12528  strressid  12530  tgvalex  12712  ptex  12713  prdsex  12718  imasex  12726  imasival  12727  imasbas  12728  imasplusg  12729  imasmulr  12730  imasaddfn  12738  imasaddval  12739  imasaddf  12740  imasmulfn  12741  imasmulval  12742  imasmulf  12743  qusval  12744  qusaddvallemg  12752  qusaddflemg  12753  qusaddval  12754  qusaddf  12755  qusmulval  12756  qusmulf  12757  mgm1  12789  0subm  12871  mhmeql  12876  grpsubval  12919  grplinv  12922  mulgval  12986  mulgfng  12987  mulg1  12990  mulgnnp1  12991  mulgnnsubcl  12995  mulgnn0subcl  12996  mulgsubcl  12997  mulgnndir  13012  subgex  13036  subgsubcl  13045  issubgrpd  13051  subsubg  13057  nsgconj  13066  0nsg  13074  triv1nsgd  13078  eqger  13083  eqgcpbl  13087  mgpex  13135  mgpf  13194  opprex  13245  opprring  13249  dvdsrex  13267  opprunitd  13279  dvrvald  13303  dvrcl  13304  unitdvcl  13305  invrpropdg  13318  subrgcrng  13346  subrgsubm  13355  subrgugrp  13361  subsubrg  13366  aprcotr  13375  rmodislmod  13441  cnsubglem  13476  iunopn  13505  toponmax  13528  tgtop  13571  tgiun  13576  tgidm  13577  ntropn  13620  tgrest  13672  restopnb  13684  cnovex  13699  cnclima  13726  txvalex  13757  txtop  13763  tx1cn  13772  tx2cn  13773  txcnp  13774  txcnmpt  13776  txdis1cn  13781  cnmptcom  13801  imasnopn  13802  hmeocnv  13810  hmeores  13818  txhmeo  13822  txswaphmeo  13824  ispsmet  13826  xmetres  13885  metres  13886  blex  13890  xmeter  13939  xmetresbl  13943  mopntopon  13946  isxms2  13955  xmetxp  14010  xmettx  14013  txmetcnp  14021  qtopbasss  14024  qtopbas  14025  reopnap  14041  ioo2blex  14047  blssioo  14048  tgioo  14049  fsumcncntop  14059  cncfval  14062  divccncfap  14080  cdivcncfap  14090  ivthdec  14125  limccnpcntop  14147  dvrecap  14180  pilem3  14207  tanrpcl  14261  cosordlem  14273  ioocosf1o  14278  rpcncxpcl  14326  rpcxpcl  14327  rpabscxpbnd  14362  rplogbcl  14367  lgslem1  14404  lgsval  14408  lgscllem  14411  lgsne0  14442  lgseisenlem1  14453  2sqlem3  14467  2sqlem8  14473  djucllem  14555  012of  14748  2o01f  14749  nninfsellemeq  14766  qdencn  14778  cvgcmp2nlemabs  14783  trilpolemclim  14787  trilpolemisumle  14789  trilpolemeq1  14791  trilpolemlt1  14792  nconstwlpolemgt0  14814