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 4851 | . . . 4 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵) | |
2 | 1 | sseq1d 4000 | . . 3 ⊢ (𝐴 = 𝐵 → (∪ 𝐴 ⊆ 𝐴 ↔ ∪ 𝐵 ⊆ 𝐴)) |
3 | sseq2 3995 | . . 3 ⊢ (𝐴 = 𝐵 → (∪ 𝐵 ⊆ 𝐴 ↔ ∪ 𝐵 ⊆ 𝐵)) | |
4 | 2, 3 | bitrd 281 | . 2 ⊢ (𝐴 = 𝐵 → (∪ 𝐴 ⊆ 𝐴 ↔ ∪ 𝐵 ⊆ 𝐵)) |
5 | df-tr 5175 | . 2 ⊢ (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴) | |
6 | df-tr 5175 | . 2 ⊢ (Tr 𝐵 ↔ ∪ 𝐵 ⊆ 𝐵) | |
7 | 4, 5, 6 | 3bitr4g 316 | 1 ⊢ (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 = wceq 1537 ⊆ wss 3938 ∪ cuni 4840 Tr wtr 5174 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-v 3498 df-in 3945 df-ss 3954 df-uni 4841 df-tr 5175 |
This theorem is referenced by: truni 5188 trint 5190 ordeq 6200 trcl 9172 tz9.1 9173 tz9.1c 9174 tctr 9184 tcmin 9185 tc2 9186 r1tr 9207 r1elssi 9236 tcrank 9315 iswun 10128 tskr1om2 10192 elgrug 10216 grutsk 10246 dfon2lem1 33030 dfon2lem3 33032 dfon2lem4 33033 dfon2lem5 33034 dfon2lem6 33035 dfon2lem7 33036 dfon2lem8 33037 dfon2 33039 dford3lem1 39630 dford3lem2 39631 |
Copyright terms: Public domain | W3C validator |