Theorem treq 5273

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

Assertion

Ref	Expression
treq	⊢ (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵))

Proof of Theorem treq

Step	Hyp	Ref	Expression
1		unieq 4919	. . . 4 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
2	1	sseq1d 4013	. . 3 ⊢ (𝐴 = 𝐵 → (∪ 𝐴 ⊆ 𝐴 ↔ ∪ 𝐵 ⊆ 𝐴))
3		sseq2 4008	. . 3 ⊢ (𝐴 = 𝐵 → (∪ 𝐵 ⊆ 𝐴 ↔ ∪ 𝐵 ⊆ 𝐵))
4	2, 3	bitrd 278	. 2 ⊢ (𝐴 = 𝐵 → (∪ 𝐴 ⊆ 𝐴 ↔ ∪ 𝐵 ⊆ 𝐵))
5		df-tr 5266	. 2 ⊢ (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴)
6		df-tr 5266	. 2 ⊢ (Tr 𝐵 ↔ ∪ 𝐵 ⊆ 𝐵)
7	4, 5, 6	3bitr4g 313	1 ⊢ (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ⊆ wss 3948  ∪ cuni 4908  Tr wtr 5265

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965  df-uni 4909  df-tr 5266

This theorem is referenced by:  truni  5281  trint  5283  ordeq  6371  trcl  9722  tz9.1  9723  tz9.1c  9724  tctr  9734  tcmin  9735  tc2  9736  r1tr  9770  r1elssi  9799  tcrank  9878  iswun  10698  tskr1om2  10762  elgrug  10786  grutsk  10816  dfon2lem1  34750  dfon2lem3  34752  dfon2lem4  34753  dfon2lem5  34754  dfon2lem6  34755  dfon2lem7  34756  dfon2lem8  34757  dfon2  34759  dford3lem1  41755  dford3lem2  41756  nadd1rabtr  42128