Theorem eqeltrrd 2218

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 2146	. 2 |- ( ph -> B = A )
3		eqeltrrd.2	. 2 |- ( ph -> A e. C )
4	2, 3	eqeltrd 2217	1 |- ( ph -> B e. C )

Syntax hints:   -> wi 4   = wceq 1332   e. wcel 1481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-clel 2136

This theorem is referenced by:  3eltr3d  2223  exmid01  4129  pwntru  4130  xpexr2m  4988  funimaexg  5215  fvmptdv2  5518  ffvresb  5591  2ndrn  6089  1st2ndbr  6090  elopabi  6101  cnvf1olem  6129  dftpos4  6168  tfrlemibxssdm  6232  tfr1onlembxssdm  6248  tfrcllembxssdm  6261  nnmordi  6420  th3qlem1  6539  infiexmid  6779  onunsnss  6813  ssfirab  6830  ssfidc  6831  fnfi  6833  fidcenumlemr  6851  elfi2  6868  ordiso2  6928  djulclb  6948  ctmlemr  7001  ctssdccl  7004  ctssdc  7006  exmidfodomrlemreseldju  7073  exmidfodomrlemr  7075  archnqq  7249  prarloclemarch2  7251  enq0tr  7266  nqnq0  7273  addcmpblnq0  7275  mulcmpblnq0  7276  mulcanenq0ec  7277  addclnq0  7283  mulclnq0  7284  nqpnq0nq  7285  nq0m0r  7288  distrnq0  7291  addassnq0lemcl  7293  prarloclemlt  7325  prarloclem5  7332  distrlem4prl  7416  distrlem4pru  7417  ltexprlemm  7432  ltexprlemrl  7442  ltexprlemru  7444  addcanprleml  7446  cauappcvgprlemladdru  7488  prsrlem1  7574  mulgt0sr  7610  axpre-suploclemres  7733  cnegexlem2  7962  subf  7988  resubcl  8050  negcon1ad  8092  subeq0bd  8165  rimul  8371  rereim  8372  aprcl  8432  nn0nnaddcl  9032  elnn0nn  9043  zaddcllemneg  9117  zsubcl  9119  zrevaddcl  9128  elz2  9146  zdiv  9163  peano5uzti  9183  peano2uzr  9407  uzaddcl  9408  divfnzn  9440  qsubcl  9457  qrevaddcl  9463  fseq1p1m1  9905  modqmuladdim  10171  frec2uzrand  10209  frecuzrdglem  10215  frecuzrdg0  10217  frecuzrdgdomlem  10221  frecuzrdg0t  10226  frecuzrdgsuctlem  10227  seq3val  10262  seq3feq  10276  iseqf1olemnab  10292  seqfeq3  10316  expaddzaplem  10367  expaddzap  10368  expmulzap  10370  zesq  10441  bcm1k  10538  bccl  10545  permnn  10549  seq3coll  10617  shftuz  10621  ref  10659  imf  10660  crre  10661  rereb  10667  resqrexlemnm  10822  absf  10914  summodclem2a  11182  summodc  11184  fsumgcl  11187  fsum3  11188  fsumf1o  11191  fsumcnv  11238  mptfzshft  11243  isumlessdc  11297  geolim2  11313  prodmodclem3  11376  fprodseq  11384  oexpneg  11610  nn0ob  11641  divalglemqt  11652  gcdf  11697  lcmgcdlem  11794  sqnprm  11852  sqrt2irrlem  11875  2sqpwodd  11890  fnum  11904  fden  11905  phimullem  11937  ctiunctlemfo  11988  unopn  12211  tsettps  12244  tgss2  12287  difopn  12316  resttop  12378  resttopon  12379  restco  12382  tgcn  12416  tgcnp  12417  cnptopco  12430  upxp  12480  txcn  12483  txdis  12485  cnmpt11  12491  cnmpt11f  12492  cnmpt1t  12493  cnmpt12  12495  cnmpt21  12499  cnmpt21f  12500  cnmpt2t  12501  cnmpt22  12502  cnmpt22f  12503  cnmpt1res  12504  xmeter  12644  mscl  12673  xmscl  12674  bdxmet  12709  cncfmpt1f  12792  cdivcncfap  12795  negfcncf  12797  cnmptlimc  12851  dvcnp2cntop  12871  sincn  12898  coscn  12899  relogcl  12991  pwtrufal  13365