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-1 5  ax-2 6  ax-3 7  ax-mp 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  4109  0ex  4110  nnc0suc  4412  nncaddccl  4419  nnsucelrlem1  4424  nndisjeq  4429  preaddccan2lem1  4454  ltfintrilem1  4465  ssfin  4470  ncfinraiselem2  4480  ncfinlowerlem1  4482  tfin0c  4497  evenoddnnnul  4514  evenodddisjlem1  4515  nnadjoinlem1  4519  nnpweqlem1  4522  sfintfinlem1  4531  tfinnnlem1  4533  vfinspss  4551  vfinspclt  4552  vfinncsp  4554  phialllem1  4616  clos1ex  5876  clos1basesuc  5882  mapexi  6003  fnpm  6008  enpw1lem1  6061  nenpw1pwlem1  6084  tc0c  6163  tc1c  6165  2nnc  6167  ce0nn  6180  ce0  6190  leconnnc  6218  nclennlem1  6248  nnltp1clem1  6261  addccan2nclem2  6264  nmembers1lem1  6268  nncdiv3lem2  6276  nnc3n3p1  6278  spacvallem1  6281  nchoicelem4  6292  nchoicelem11  6299  nchoicelem12  6300  nchoicelem16  6304  nchoicelem17  6305  nchoicelem18  6306