Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > treq | Structured version Visualization version GIF version |
Description: Equality theorem for the transitive class predicate. (Contributed by NM, 17-Sep-1993.) |
Ref | Expression |
---|---|
treq | ⊢ (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unieq 4444 | . . . 4 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵) | |
2 | 1 | sseq1d 3632 | . . 3 ⊢ (𝐴 = 𝐵 → (∪ 𝐴 ⊆ 𝐴 ↔ ∪ 𝐵 ⊆ 𝐴)) |
3 | sseq2 3627 | . . 3 ⊢ (𝐴 = 𝐵 → (∪ 𝐵 ⊆ 𝐴 ↔ ∪ 𝐵 ⊆ 𝐵)) | |
4 | 2, 3 | bitrd 268 | . 2 ⊢ (𝐴 = 𝐵 → (∪ 𝐴 ⊆ 𝐴 ↔ ∪ 𝐵 ⊆ 𝐵)) |
5 | df-tr 4753 | . 2 ⊢ (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴) | |
6 | df-tr 4753 | . 2 ⊢ (Tr 𝐵 ↔ ∪ 𝐵 ⊆ 𝐵) | |
7 | 4, 5, 6 | 3bitr4g 303 | 1 ⊢ (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 = wceq 1483 ⊆ wss 3574 ∪ cuni 4436 Tr wtr 4752 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rex 2918 df-in 3581 df-ss 3588 df-uni 4437 df-tr 4753 |
This theorem is referenced by: truni 4767 ordeq 5730 trcl 8604 tz9.1 8605 tz9.1c 8606 tctr 8616 tcmin 8617 tc2 8618 r1tr 8639 r1elssi 8668 tcrank 8747 iswun 9526 tskr1om2 9590 elgrug 9614 grutsk 9644 dfon2lem1 31688 dfon2lem3 31690 dfon2lem4 31691 dfon2lem5 31692 dfon2lem6 31693 dfon2lem7 31694 dfon2lem8 31695 dfon2 31697 dford3lem1 37593 dford3lem2 37594 |
Copyright terms: Public domain | W3C validator |