Theorem eqeltrrd 2271

Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)

Hypotheses

Ref	Expression
eqeltrrd.1	|- ( ph -> A = B )
eqeltrrd.2	|- ( ph -> A e. C )

Assertion

Ref	Expression
eqeltrrd	|- ( ph -> B e. C )

Proof of Theorem eqeltrrd

Step	Hyp	Ref	Expression
1		eqeltrrd.1	. . 3 |- ( ph -> A = B )
2	1	eqcomd 2199	. 2 |- ( ph -> B = A )
3		eqeltrrd.2	. 2 |- ( ph -> A e. C )
4	2, 3	eqeltrd 2270	1 |- ( ph -> B e. C )

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

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 2175

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

This theorem is referenced by:  3eltr3d  2276  exmid01  4227  pwntru  4228  xpexr2m  5107  funimaexg  5338  fvmptdv2  5647  ffvresb  5721  iotaexel  5878  2ndrn  6236  1st2ndbr  6237  elopabi  6248  cnvf1olem  6277  dftpos4  6316  tfrlemibxssdm  6380  tfr1onlembxssdm  6396  tfrcllembxssdm  6409  nnmordi  6569  th3qlem1  6691  infiexmid  6933  onunsnss  6973  ssfirab  6990  ssfidc  6991  fnfi  6995  fidcenumlemr  7014  elfi2  7031  ordiso2  7094  djulclb  7114  ctmlemr  7167  ctssdccl  7170  ctssdc  7172  exmidfodomrlemreseldju  7260  exmidfodomrlemr  7262  exmidapne  7320  archnqq  7477  prarloclemarch2  7479  enq0tr  7494  nqnq0  7501  addcmpblnq0  7503  mulcmpblnq0  7504  mulcanenq0ec  7505  addclnq0  7511  mulclnq0  7512  nqpnq0nq  7513  nq0m0r  7516  distrnq0  7519  addassnq0lemcl  7521  prarloclemlt  7553  prarloclem5  7560  distrlem4prl  7644  distrlem4pru  7645  ltexprlemm  7660  ltexprlemrl  7670  ltexprlemru  7672  addcanprleml  7674  cauappcvgprlemladdru  7716  prsrlem1  7802  mulgt0sr  7838  axpre-suploclemres  7961  cnegexlem2  8195  subf  8221  resubcl  8283  negcon1ad  8325  subeq0bd  8398  rimul  8604  rereim  8605  aprcl  8665  nn0nnaddcl  9271  elnn0nn  9282  zaddcllemneg  9356  zsubcl  9358  zrevaddcl  9367  elz2  9388  zdiv  9405  peano5uzti  9425  peano2uzr  9650  uzaddcl  9651  divfnzn  9686  qsubcl  9703  qrevaddcl  9709  fseq1p1m1  10160  modqmuladdim  10438  frec2uzrand  10476  frecuzrdglem  10482  frecuzrdg0  10484  frecuzrdgdomlem  10488  frecuzrdg0t  10493  frecuzrdgsuctlem  10494  seq3val  10531  seq3feq  10551  iseqf1olemnab  10572  seqf1oglem2  10591  seqfeq3  10600  seqfeq4g  10602  expaddzaplem  10653  expaddzap  10654  expmulzap  10656  zesq  10729  bcm1k  10831  bccl  10838  permnn  10842  seq3coll  10913  shftuz  10961  ref  10999  imf  11000  crre  11001  rereb  11007  resqrexlemnm  11162  absf  11254  summodclem2a  11524  summodc  11526  fsumgcl  11529  fsum3  11530  fsumf1o  11533  fsumcnv  11580  mptfzshft  11585  isumlessdc  11639  geolim2  11655  prodmodclem3  11718  fprodseq  11726  fprodf1o  11731  dvdsaddre2b  11984  oexpneg  12018  nn0ob  12049  divalglemqt  12060  suprzubdc  12089  gcdf  12109  lcmgcdlem  12215  sqnprm  12274  sqrt2irrlem  12299  2sqpwodd  12314  fnum  12328  fden  12329  phimullem  12363  pc2dvds  12468  gzsubcl  12518  4sqlem5  12520  4sqlem9  12524  4sqlem10  12525  mul4sqlem  12531  mul4sq  12532  4sqlem11  12539  4sqlem13m  12541  4sqlem16  12544  4sqlem17  12545  4sqlem18  12546  ctiunctlemfo  12596  ptex  12875  mgmsscl  12944  subsubm  13055  mhmima  13063  imasgrp2  13180  mhmmnd  13186  mulgdir  13224  subgmulg  13258  issubg2m  13259  issubgrpd2  13260  grpissubg  13264  subsubg  13267  isnsg3  13277  ssnmz  13281  eqger  13294  eqgen  13297  ecqusaddcl  13309  ghmrn  13327  ghmnsgima  13338  conjsubg  13347  conjnmz  13349  ring1  13555  reldvdsrsrg  13588  dvdsrvald  13589  dvdsrd  13590  dvdsrex  13594  0unit  13625  invrpropdg  13645  lringuplu  13692  subrngin  13709  subsubrng  13710  subrgcrng  13721  subrgin  13740  subsubrg  13741  islmodd  13789  lssvacl  13861  lssvancl1  13863  lss0cl  13865  lssvscl  13871  lssvnegcl  13872  lssincl  13881  issubrgd  13948  lidlrsppropdg  13991  2idlcpblrng  14019  zsssubrg  14073  unopn  14173  tsettps  14206  tgss2  14247  difopn  14276  resttop  14338  resttopon  14339  restco  14342  tgcn  14376  tgcnp  14377  cnptopco  14390  upxp  14440  txcn  14443  txdis  14445  cnmpt11  14451  cnmpt11f  14452  cnmpt1t  14453  cnmpt12  14455  cnmpt21  14459  cnmpt21f  14460  cnmpt2t  14461  cnmpt22  14462  cnmpt22f  14463  cnmpt1res  14464  xmeter  14604  mscl  14633  xmscl  14634  bdxmet  14669  cncfmpt1f  14752  cdivcncfap  14758  negfcncf  14760  ivthreinc  14799  cnmptlimc  14828  dvcnp2cntop  14848  elplyd  14887  plypow  14890  plyconst  14891  plyaddlem1  14893  plysub  14899  sincn  14904  coscn  14905  relogcl  14997  lgsne0  15154  lgseisenlem4  15189  lgsquadlem1  15191  pwtrufal  15488