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  4232  pwntru  4233  xpexr2m  5112  funimaexg  5343  fvmptdv2  5654  ffvresb  5728  iotaexel  5885  2ndrn  6250  1st2ndbr  6251  elopabi  6262  cnvf1olem  6291  dftpos4  6330  tfrlemibxssdm  6394  tfr1onlembxssdm  6410  tfrcllembxssdm  6423  nnmordi  6583  th3qlem1  6705  infiexmid  6947  onunsnss  6987  ssfirab  7006  ssfidc  7007  fnfi  7011  fidcenumlemr  7030  elfi2  7047  ordiso2  7110  djulclb  7130  ctmlemr  7183  ctssdccl  7186  ctssdc  7188  exmidfodomrlemreseldju  7279  exmidfodomrlemr  7281  exmidapne  7343  archnqq  7501  prarloclemarch2  7503  enq0tr  7518  nqnq0  7525  addcmpblnq0  7527  mulcmpblnq0  7528  mulcanenq0ec  7529  addclnq0  7535  mulclnq0  7536  nqpnq0nq  7537  nq0m0r  7540  distrnq0  7543  addassnq0lemcl  7545  prarloclemlt  7577  prarloclem5  7584  distrlem4prl  7668  distrlem4pru  7669  ltexprlemm  7684  ltexprlemrl  7694  ltexprlemru  7696  addcanprleml  7698  cauappcvgprlemladdru  7740  prsrlem1  7826  mulgt0sr  7862  axpre-suploclemres  7985  cnegexlem2  8219  subf  8245  resubcl  8307  negcon1ad  8349  subeq0bd  8422  rimul  8629  rereim  8630  aprcl  8690  nn0nnaddcl  9297  elnn0nn  9308  zaddcllemneg  9382  zsubcl  9384  zrevaddcl  9393  elz2  9414  zdiv  9431  peano5uzti  9451  peano2uzr  9676  uzaddcl  9677  divfnzn  9712  qsubcl  9729  qrevaddcl  9735  fseq1p1m1  10186  suprzubdc  10343  modqmuladdim  10476  frec2uzrand  10514  frecuzrdglem  10520  frecuzrdg0  10522  frecuzrdgdomlem  10526  frecuzrdg0t  10531  frecuzrdgsuctlem  10532  seq3val  10569  seq3feq  10589  iseqf1olemnab  10610  seqf1oglem2  10629  seqfeq3  10638  seqfeq4g  10640  expaddzaplem  10691  expaddzap  10692  expmulzap  10694  zesq  10767  bcm1k  10869  bccl  10876  permnn  10880  seq3coll  10951  shftuz  10999  ref  11037  imf  11038  crre  11039  rereb  11045  resqrexlemnm  11200  absf  11292  summodclem2a  11563  summodc  11565  fsumgcl  11568  fsum3  11569  fsumf1o  11572  fsumcnv  11619  mptfzshft  11624  isumlessdc  11678  geolim2  11694  prodmodclem3  11757  fprodseq  11765  fprodf1o  11770  dvdsaddre2b  12023  3dvds  12046  oexpneg  12059  nn0ob  12090  divalglemqt  12101  gcdf  12164  lcmgcdlem  12270  sqnprm  12329  sqrt2irrlem  12354  2sqpwodd  12369  fnum  12383  fden  12384  phimullem  12418  pc2dvds  12524  gzsubcl  12574  4sqlem5  12576  4sqlem9  12580  4sqlem10  12581  mul4sqlem  12587  mul4sq  12588  4sqlem11  12595  4sqlem13m  12597  4sqlem16  12600  4sqlem17  12601  4sqlem18  12602  ctiunctlemfo  12681  ptex  12966  prdsval  12975  prdsbas  12978  prdsbascl  12991  mgmsscl  13063  subsubm  13185  mhmima  13193  imasgrp2  13316  mhmmnd  13322  mulgdir  13360  subgmulg  13394  issubg2m  13395  issubgrpd2  13396  grpissubg  13400  subsubg  13403  isnsg3  13413  ssnmz  13417  eqger  13430  eqgen  13433  ecqusaddcl  13445  ghmrn  13463  ghmnsgima  13474  conjsubg  13483  conjnmz  13485  ring1  13691  reldvdsrsrg  13724  dvdsrvald  13725  dvdsrd  13726  dvdsrex  13730  0unit  13761  invrpropdg  13781  lringuplu  13828  subrngin  13845  subsubrng  13846  subrgcrng  13857  subrgin  13876  subsubrg  13877  islmodd  13925  lssvacl  13997  lssvancl1  13999  lss0cl  14001  lssvscl  14007  lssvnegcl  14008  lssincl  14017  issubrgd  14084  lidlrsppropdg  14127  2idlcpblrng  14155  zsssubrg  14217  unopn  14325  tsettps  14358  tgss2  14399  difopn  14428  resttop  14490  resttopon  14491  restco  14494  tgcn  14528  tgcnp  14529  cnptopco  14542  upxp  14592  txcn  14595  txdis  14597  cnmpt11  14603  cnmpt11f  14604  cnmpt1t  14605  cnmpt12  14607  cnmpt21  14611  cnmpt21f  14612  cnmpt2t  14613  cnmpt22  14614  cnmpt22f  14615  cnmpt1res  14616  xmeter  14756  mscl  14785  xmscl  14786  bdxmet  14821  cncfmpt1f  14918  cdivcncfap  14924  negfcncf  14926  ivthreinc  14965  cnmptlimc  14994  dvcnp2cntop  15019  elplyd  15061  plypow  15064  plyconst  15065  plyaddlem1  15067  plysub  15073  dvply2g  15086  sincn  15089  coscn  15090  relogcl  15182  mpodvdsmulf1o  15310  fsumdvdsmul  15311  mersenne  15317  perfect  15321  lgsne0  15363  lgseisenlem4  15398  lgsquadlem1  15402  pwtrufal  15728