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 4848 | . . . 4 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵) | |
2 | 1 | sseq1d 3997 | . . 3 ⊢ (𝐴 = 𝐵 → (∪ 𝐴 ⊆ 𝐴 ↔ ∪ 𝐵 ⊆ 𝐴)) |
3 | sseq2 3992 | . . 3 ⊢ (𝐴 = 𝐵 → (∪ 𝐵 ⊆ 𝐴 ↔ ∪ 𝐵 ⊆ 𝐵)) | |
4 | 2, 3 | bitrd 281 | . 2 ⊢ (𝐴 = 𝐵 → (∪ 𝐴 ⊆ 𝐴 ↔ ∪ 𝐵 ⊆ 𝐵)) |
5 | df-tr 5172 | . 2 ⊢ (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴) | |
6 | df-tr 5172 | . 2 ⊢ (Tr 𝐵 ↔ ∪ 𝐵 ⊆ 𝐵) | |
7 | 4, 5, 6 | 3bitr4g 316 | 1 ⊢ (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 = wceq 1533 ⊆ wss 3935 ∪ cuni 4837 Tr wtr 5171 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-v 3496 df-in 3942 df-ss 3951 df-uni 4838 df-tr 5172 |
This theorem is referenced by: truni 5185 trint 5187 ordeq 6197 trcl 9169 tz9.1 9170 tz9.1c 9171 tctr 9181 tcmin 9182 tc2 9183 r1tr 9204 r1elssi 9233 tcrank 9312 iswun 10125 tskr1om2 10189 elgrug 10213 grutsk 10243 dfon2lem1 33028 dfon2lem3 33030 dfon2lem4 33031 dfon2lem5 33032 dfon2lem6 33033 dfon2lem7 33034 dfon2lem8 33035 dfon2 33037 dford3lem1 39621 dford3lem2 39622 |
Copyright terms: Public domain | W3C validator |