Theorem eqeltrrd 2274

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 2202	. 2 |- ( ph -> B = A )
3		eqeltrrd.2	. 2 |- ( ph -> A e. C )
4	2, 3	eqeltrd 2273	1 |- ( ph -> B 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:  3eltr3d  2279  exmid01  4231  pwntru  4232  xpexr2m  5111  funimaexg  5342  fvmptdv2  5651  ffvresb  5725  iotaexel  5882  2ndrn  6241  1st2ndbr  6242  elopabi  6253  cnvf1olem  6282  dftpos4  6321  tfrlemibxssdm  6385  tfr1onlembxssdm  6401  tfrcllembxssdm  6414  nnmordi  6574  th3qlem1  6696  infiexmid  6938  onunsnss  6978  ssfirab  6997  ssfidc  6998  fnfi  7002  fidcenumlemr  7021  elfi2  7038  ordiso2  7101  djulclb  7121  ctmlemr  7174  ctssdccl  7177  ctssdc  7179  exmidfodomrlemreseldju  7267  exmidfodomrlemr  7269  exmidapne  7327  archnqq  7484  prarloclemarch2  7486  enq0tr  7501  nqnq0  7508  addcmpblnq0  7510  mulcmpblnq0  7511  mulcanenq0ec  7512  addclnq0  7518  mulclnq0  7519  nqpnq0nq  7520  nq0m0r  7523  distrnq0  7526  addassnq0lemcl  7528  prarloclemlt  7560  prarloclem5  7567  distrlem4prl  7651  distrlem4pru  7652  ltexprlemm  7667  ltexprlemrl  7677  ltexprlemru  7679  addcanprleml  7681  cauappcvgprlemladdru  7723  prsrlem1  7809  mulgt0sr  7845  axpre-suploclemres  7968  cnegexlem2  8202  subf  8228  resubcl  8290  negcon1ad  8332  subeq0bd  8405  rimul  8612  rereim  8613  aprcl  8673  nn0nnaddcl  9280  elnn0nn  9291  zaddcllemneg  9365  zsubcl  9367  zrevaddcl  9376  elz2  9397  zdiv  9414  peano5uzti  9434  peano2uzr  9659  uzaddcl  9660  divfnzn  9695  qsubcl  9712  qrevaddcl  9718  fseq1p1m1  10169  suprzubdc  10326  modqmuladdim  10459  frec2uzrand  10497  frecuzrdglem  10503  frecuzrdg0  10505  frecuzrdgdomlem  10509  frecuzrdg0t  10514  frecuzrdgsuctlem  10515  seq3val  10552  seq3feq  10572  iseqf1olemnab  10593  seqf1oglem2  10612  seqfeq3  10621  seqfeq4g  10623  expaddzaplem  10674  expaddzap  10675  expmulzap  10677  zesq  10750  bcm1k  10852  bccl  10859  permnn  10863  seq3coll  10934  shftuz  10982  ref  11020  imf  11021  crre  11022  rereb  11028  resqrexlemnm  11183  absf  11275  summodclem2a  11546  summodc  11548  fsumgcl  11551  fsum3  11552  fsumf1o  11555  fsumcnv  11602  mptfzshft  11607  isumlessdc  11661  geolim2  11677  prodmodclem3  11740  fprodseq  11748  fprodf1o  11753  dvdsaddre2b  12006  3dvds  12029  oexpneg  12042  nn0ob  12073  divalglemqt  12084  gcdf  12139  lcmgcdlem  12245  sqnprm  12304  sqrt2irrlem  12329  2sqpwodd  12344  fnum  12358  fden  12359  phimullem  12393  pc2dvds  12499  gzsubcl  12549  4sqlem5  12551  4sqlem9  12555  4sqlem10  12556  mul4sqlem  12562  mul4sq  12563  4sqlem11  12570  4sqlem13m  12572  4sqlem16  12575  4sqlem17  12576  4sqlem18  12577  ctiunctlemfo  12656  ptex  12935  mgmsscl  13004  subsubm  13115  mhmima  13123  imasgrp2  13240  mhmmnd  13246  mulgdir  13284  subgmulg  13318  issubg2m  13319  issubgrpd2  13320  grpissubg  13324  subsubg  13327  isnsg3  13337  ssnmz  13341  eqger  13354  eqgen  13357  ecqusaddcl  13369  ghmrn  13387  ghmnsgima  13398  conjsubg  13407  conjnmz  13409  ring1  13615  reldvdsrsrg  13648  dvdsrvald  13649  dvdsrd  13650  dvdsrex  13654  0unit  13685  invrpropdg  13705  lringuplu  13752  subrngin  13769  subsubrng  13770  subrgcrng  13781  subrgin  13800  subsubrg  13801  islmodd  13849  lssvacl  13921  lssvancl1  13923  lss0cl  13925  lssvscl  13931  lssvnegcl  13932  lssincl  13941  issubrgd  14008  lidlrsppropdg  14051  2idlcpblrng  14079  zsssubrg  14141  unopn  14241  tsettps  14274  tgss2  14315  difopn  14344  resttop  14406  resttopon  14407  restco  14410  tgcn  14444  tgcnp  14445  cnptopco  14458  upxp  14508  txcn  14511  txdis  14513  cnmpt11  14519  cnmpt11f  14520  cnmpt1t  14521  cnmpt12  14523  cnmpt21  14527  cnmpt21f  14528  cnmpt2t  14529  cnmpt22  14530  cnmpt22f  14531  cnmpt1res  14532  xmeter  14672  mscl  14701  xmscl  14702  bdxmet  14737  cncfmpt1f  14834  cdivcncfap  14840  negfcncf  14842  ivthreinc  14881  cnmptlimc  14910  dvcnp2cntop  14935  elplyd  14977  plypow  14980  plyconst  14981  plyaddlem1  14983  plysub  14989  dvply2g  15002  sincn  15005  coscn  15006  relogcl  15098  mpodvdsmulf1o  15226  fsumdvdsmul  15227  mersenne  15233  perfect  15237  lgsne0  15279  lgseisenlem4  15314  lgsquadlem1  15318  pwtrufal  15642