![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > treq | Unicode version |
Description: Equality theorem for the transitive class predicate. (Contributed by NM, 17-Sep-1993.) |
Ref | Expression |
---|---|
treq |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unieq 3984 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | sseq1d 3335 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | sseq2 3330 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | bitrd 245 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | df-tr 4263 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | df-tr 4263 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 4, 5, 6 | 3bitr4g 280 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem is referenced by: truni 4276 ordeq 4548 trcl 7620 tz9.1 7621 tz9.1c 7622 tctr 7635 tcmin 7636 tc2 7637 r1tr 7658 r1elssi 7687 tcrank 7764 iswun 8535 tskr1om2 8599 elgrug 8623 grutsk 8653 dfon2lem1 25353 dfon2lem3 25355 dfon2lem4 25356 dfon2lem5 25357 dfon2lem6 25358 dfon2lem7 25359 dfon2lem8 25360 dfon2 25362 dford3lem1 26987 dford3lem2 26988 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 |
This theorem depends on definitions: df-bi 178 df-an 361 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-rex 2672 df-in 3287 df-ss 3294 df-uni 3976 df-tr 4263 |
Copyright terms: Public domain | W3C validator |