Theorem eqeltrri 2424

Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
eqeltrr.1	⊢ A = B
eqeltrr.2	⊢ A ∈ C

Assertion

Ref	Expression
eqeltrri	⊢ B ∈ C

Proof of Theorem eqeltrri

Step	Hyp	Ref	Expression
1		eqeltrr.1	. . 3 ⊢ A = B
2	1	eqcomi 2357	. 2 ⊢ B = A
3		eqeltrr.2	. 2 ⊢ A ∈ C
4	2, 3	eqeltri 2423	1 ⊢ B ∈ C

Syntax hints:   = wceq 1642   ∈ wcel 1710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-cleq 2346  df-clel 2349

This theorem is referenced by:  3eltr3i  2431  vvex  4110  0ex  4111  nnc0suc  4413  nncaddccl  4420  nnsucelrlem1  4425  nndisjeq  4430  preaddccan2lem1  4455  ltfintrilem1  4466  ssfin  4471  ncfinraiselem2  4481  ncfinlowerlem1  4483  tfin0c  4498  evenoddnnnul  4515  evenodddisjlem1  4516  nnadjoinlem1  4520  nnpweqlem1  4523  sfintfinlem1  4532  tfinnnlem1  4534  vfinspss  4552  vfinspclt  4553  vfinncsp  4555  phialllem1  4617  clos1ex  5877  clos1basesuc  5883  mapexi  6004  fnpm  6009  enpw1lem1  6062  nenpw1pwlem1  6085  tc0c  6164  tc1c  6166  2nnc  6168  ce0nn  6181  ce0  6191  leconnnc  6219  nclennlem1  6249  nnltp1clem1  6262  addccan2nclem2  6265  nmembers1lem1  6269  nncdiv3lem2  6277  nnc3n3p1  6279  spacvallem1  6282  nchoicelem4  6293  nchoicelem11  6300  nchoicelem12  6301  nchoicelem16  6305  nchoicelem17  6306  nchoicelem18  6307