New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  eqeltrri GIF version

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
StepHypRef Expression
1 eqeltrr.1 . . 3 A = B
21eqcomi 2357 . 2 B = A
3 eqeltrr.2 . 2 A C
42, 3eqeltri 2423 1 B C
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator