Theorem eqeltrrd 2316

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   e. wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  3eltr3d  2321  exmid01  4335  pwntru  4336  xpexr2m  5229  funimaexg  5465  fndmexd  5581  fvmptdv2  5795  ffvresb  5871  iotaexel  6043  2ndrn  6417  1st2ndbr  6418  elopabi  6431  cnvf1olem  6460  dftpos4  6534  tfrlemibxssdm  6598  tfr1onlembxssdm  6614  tfrcllembxssdm  6627  nnmordi  6789  th3qlem1  6911  infiexmid  7181  onunsnss  7224  ssfirab  7244  ssfidc  7245  fnfi  7250  fidcenumlemr  7272  elfi2  7306  f1setfi  7317  ordiso2  7376  djulclb  7396  ctmlemr  7449  ctssdccl  7452  ctssdc  7454  exmidfodomrlemreseldju  7553  exmidfodomrlemr  7555  pw1m  7584  exmidapne  7627  archnqq  7785  prarloclemarch2  7787  enq0tr  7802  nqnq0  7809  addcmpblnq0  7811  mulcmpblnq0  7812  mulcanenq0ec  7813  addclnq0  7819  mulclnq0  7820  nqpnq0nq  7821  nq0m0r  7824  distrnq0  7827  addassnq0lemcl  7829  prarloclemlt  7861  prarloclem5  7868  distrlem4prl  7952  distrlem4pru  7953  ltexprlemm  7968  ltexprlemrl  7978  ltexprlemru  7980  addcanprleml  7982  cauappcvgprlemladdru  8024  prsrlem1  8110  mulgt0sr  8146  axpre-suploclemres  8269  cnegexlem2  8504  subf  8530  resubcl  8592  negcon1ad  8634  subeq0bd  8708  rimul  8916  rereim  8917  aprcl  8977  nn0nnaddcl  9599  elnn0nn  9610  zaddcllemneg  9688  zsubcl  9690  zrevaddcl  9700  elz2  9721  zdiv  9739  peano5uzti  9759  peano2uzr  9995  uzaddcl  9996  divfnzn  10031  qsubcl  10048  qrevaddcl  10054  fseq1p1m1  10512  suprzubdc  10682  modqmuladdim  10819  frec2uzrand  10857  frecuzrdglem  10863  frecuzrdg0  10865  frecuzrdgdomlem  10869  frecuzrdg0t  10874  frecuzrdgsuctlem  10875  seq3val  10912  seq3feq  10932  iseqf1olemnab  10953  seqf1oglem2  10972  seqfeq3  10981  seqfeq4g  10983  expaddzaplem  11034  expaddzap  11035  expmulzap  11037  zesq  11111  bcm1k  11214  bccl  11221  permnn  11226  hashf1lem2  11302  hashf1  11303  seq3coll  11310  ccatrn  11393  shftuz  11598  ref  11636  imf  11637  crre  11638  rereb  11644  resqrexlemnm  11800  absf  11893  summodclem2a  12167  summodc  12169  fsumgcl  12172  fsum3  12173  fsumf1o  12176  fsumcnv  12223  mptfzshft  12228  isumlessdc  12282  geolim2  12298  prodmodclem3  12361  fprodseq  12369  fprodf1o  12374  dvdsaddre2b  12627  3dvds  12650  oexpneg  12663  nn0ob  12694  divalglemqt  12705  gcdf  12768  lcmgcdlem  12874  sqnprm  12934  sqrt2irrlem  12959  2sqpwodd  12975  fnum  12989  fden  12990  nn0sqdcq  13007  phimullem  13026  pc2dvds  13132  gzsubcl  13182  4sqlem5  13184  4sqlem9  13188  4sqlem10  13189  mul4sqlem  13195  mul4sq  13196  4sqlem11  13203  4sqlem13m  13205  4sqlem16  13208  4sqlem17  13209  4sqlem18  13210  ballotfilem2  13280  ballotfilemsf1o  13309  ballotfilemrinv0  13328  ctiunctlemfo  13382  ptex  13671  mgmsscl  13734  subsubm  13843  mhmima  13851  imasgrp2  13966  mhmmnd  13972  mulgdir  14010  subgmulg  14044  issubg2m  14045  issubgrpd2  14046  grpissubg  14050  subsubg  14053  isnsg3  14063  ssnmz  14067  eqger  14080  eqgen  14083  ecqusaddcl  14095  ghmrn  14113  ghmnsgima  14124  conjsubg  14133  conjnmz  14135  gsumclfi  14243  gsumsubmclfi  14247  prdsval  14257  prdsbas  14260  prdsbascl  14273  ring1  14448  dvdsrvald  14484  dvdsrd  14485  dvdsrex  14489  0unit  14520  invrpropdg  14540  lringuplu  14587  subrngin  14605  subsubrng  14606  subrgcrng  14617  subrgin  14636  subsubrg  14637  aprnzr  14683  aprlring  14684  islmodd  14713  lssvacl  14786  lssvancl1  14788  lss0cl  14790  lssvscl  14796  lssvnegcl  14797  lssincl  14806  issubrgd  14873  lidlrsppropdg  14916  2idlcpblrng  14944  zsssubrg  15006  issubassa2  15119  psrbaglefifi  15147  unopn  15197  tsettps  15230  tgss2  15271  difopn  15300  resttop  15362  resttopon  15363  restco  15366  tgcn  15400  tgcnp  15401  cnptopco  15414  upxp  15464  txcn  15467  txdis  15469  cnmpt11  15475  cnmpt11f  15476  cnmpt1t  15477  cnmpt12  15479  cnmpt21  15483  cnmpt21f  15484  cnmpt2t  15485  cnmpt22  15486  cnmpt22f  15487  cnmpt1res  15488  xmeter  15628  mscl  15657  xmscl  15658  bdxmet  15693  cncfmpt1f  15790  cdivcncfap  15796  negfcncf  15798  ivthreinc  15837  cnmptlimc  15866  dvcnp2cntop  15891  elplyd  15933  plypow  15936  plyconst  15937  plyaddlem1  15939  plysub  15945  dvply2g  15958  sincn  15961  coscn  15962  relogcl  16055  ppiprm  16220  ppinprm  16221  chtprm  16222  chtnprm  16223  efchtqdvds  16226  prmorcht  16243  mpodvdsmulf1o  16245  fsumdvdsmul  16246  chtublem  16256  mersenne  16258  perfect  16262  lgsne0  16323  lgseisenlem4  16358  lgsquadlem1  16362  usgr1vr  16655  p1evtxdeqfilem  16718  isclwwlkn  16820  clwwlknon  16836  pwtrufal  17193  repiecele0  17241  qdiff  17265