This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem treq

Description: Equality theorem for the transitive class predicate. (Contributed by NM, 17-Sep-1993)

Ref Expression
Assertion treq ⊢ A = B → Tr ⁡ A ↔ Tr ⁡ B

Proof

Step Hyp Ref Expression
1 unieq ⊢ A = B → ⋃ A = ⋃ B
2 1 sseq1d ⊢ A = B → ⋃ A ⊆ A ↔ ⋃ B ⊆ A
3 sseq2 ⊢ A = B → ⋃ B ⊆ A ↔ ⋃ B ⊆ B
4 2 3 bitrd ⊢ A = B → ⋃ A ⊆ A ↔ ⋃ B ⊆ B
5 df-tr ⊢ Tr ⁡ A ↔ ⋃ A ⊆ A
6 df-tr ⊢ Tr ⁡ B ↔ ⋃ B ⊆ B
7 4 5 6 3bitr4g ⊢ A = B → Tr ⁡ A ↔ Tr ⁡ B