Theorem eqeltrrd 2255

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 2183	. 2 |- ( ph -> B = A )
3		eqeltrrd.2	. 2 |- ( ph -> A e. C )
4	2, 3	eqeltrd 2254	1 |- ( ph -> B 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:  3eltr3d  2260  exmid01  4200  pwntru  4201  xpexr2m  5072  funimaexg  5302  fvmptdv2  5607  ffvresb  5681  2ndrn  6186  1st2ndbr  6187  elopabi  6198  cnvf1olem  6227  dftpos4  6266  tfrlemibxssdm  6330  tfr1onlembxssdm  6346  tfrcllembxssdm  6359  nnmordi  6519  th3qlem1  6639  infiexmid  6879  onunsnss  6918  ssfirab  6935  ssfidc  6936  fnfi  6938  fidcenumlemr  6956  elfi2  6973  ordiso2  7036  djulclb  7056  ctmlemr  7109  ctssdccl  7112  ctssdc  7114  exmidfodomrlemreseldju  7201  exmidfodomrlemr  7203  exmidapne  7261  archnqq  7418  prarloclemarch2  7420  enq0tr  7435  nqnq0  7442  addcmpblnq0  7444  mulcmpblnq0  7445  mulcanenq0ec  7446  addclnq0  7452  mulclnq0  7453  nqpnq0nq  7454  nq0m0r  7457  distrnq0  7460  addassnq0lemcl  7462  prarloclemlt  7494  prarloclem5  7501  distrlem4prl  7585  distrlem4pru  7586  ltexprlemm  7601  ltexprlemrl  7611  ltexprlemru  7613  addcanprleml  7615  cauappcvgprlemladdru  7657  prsrlem1  7743  mulgt0sr  7779  axpre-suploclemres  7902  cnegexlem2  8135  subf  8161  resubcl  8223  negcon1ad  8265  subeq0bd  8338  rimul  8544  rereim  8545  aprcl  8605  nn0nnaddcl  9209  elnn0nn  9220  zaddcllemneg  9294  zsubcl  9296  zrevaddcl  9305  elz2  9326  zdiv  9343  peano5uzti  9363  peano2uzr  9587  uzaddcl  9588  divfnzn  9623  qsubcl  9640  qrevaddcl  9646  fseq1p1m1  10096  modqmuladdim  10369  frec2uzrand  10407  frecuzrdglem  10413  frecuzrdg0  10415  frecuzrdgdomlem  10419  frecuzrdg0t  10424  frecuzrdgsuctlem  10425  seq3val  10460  seq3feq  10474  iseqf1olemnab  10490  seqfeq3  10514  expaddzaplem  10565  expaddzap  10566  expmulzap  10568  zesq  10641  bcm1k  10742  bccl  10749  permnn  10753  seq3coll  10824  shftuz  10828  ref  10866  imf  10867  crre  10868  rereb  10874  resqrexlemnm  11029  absf  11121  summodclem2a  11391  summodc  11393  fsumgcl  11396  fsum3  11397  fsumf1o  11400  fsumcnv  11447  mptfzshft  11452  isumlessdc  11506  geolim2  11522  prodmodclem3  11585  fprodseq  11593  fprodf1o  11598  dvdsaddre2b  11850  oexpneg  11884  nn0ob  11915  divalglemqt  11926  suprzubdc  11955  gcdf  11975  lcmgcdlem  12079  sqnprm  12138  sqrt2irrlem  12163  2sqpwodd  12178  fnum  12192  fden  12193  phimullem  12227  pc2dvds  12331  gzsubcl  12380  4sqlem5  12382  4sqlem9  12386  4sqlem10  12387  mul4sqlem  12393  mul4sq  12394  ctiunctlemfo  12442  ptex  12718  mgmsscl  12785  mhmima  12880  mhmmnd  12985  mulgdir  13020  subgmulg  13053  issubg2m  13054  issubgrpd2  13055  grpissubg  13059  subsubg  13062  isnsg3  13072  ssnmz  13076  eqger  13088  eqgen  13091  ring1  13241  reldvdsrsrg  13266  dvdsrvald  13267  dvdsrd  13268  dvdsrex  13272  0unit  13303  invrpropdg  13323  lringuplu  13342  subrgcrng  13351  subrgin  13370  subsubrg  13371  islmodd  13388  lssvancl1  13458  lss0cl  13460  lssvacl  13466  lssvscl  13467  lssvnegcl  13468  lssincl  13477  zsssubrg  13564  unopn  13590  tsettps  13623  tgss2  13664  difopn  13693  resttop  13755  resttopon  13756  restco  13759  tgcn  13793  tgcnp  13794  cnptopco  13807  upxp  13857  txcn  13860  txdis  13862  cnmpt11  13868  cnmpt11f  13869  cnmpt1t  13870  cnmpt12  13872  cnmpt21  13876  cnmpt21f  13877  cnmpt2t  13878  cnmpt22  13879  cnmpt22f  13880  cnmpt1res  13881  xmeter  14021  mscl  14050  xmscl  14051  bdxmet  14086  cncfmpt1f  14169  cdivcncfap  14172  negfcncf  14174  cnmptlimc  14228  dvcnp2cntop  14248  sincn  14275  coscn  14276  relogcl  14368  lgsne0  14524  pwtrufal  14832