![]() |
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > NFE Home > Th. List > eqeltrri | GIF version |
Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eqeltrr.1 | ⊢ A = B |
eqeltrr.2 | ⊢ A ∈ C |
Ref | Expression |
---|---|
eqeltrri | ⊢ B ∈ C |
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 |
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 |