Theorem treq 5237

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 4894	. . . 4 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
2	1	sseq1d 3990	. . 3 ⊢ (𝐴 = 𝐵 → (∪ 𝐴 ⊆ 𝐴 ↔ ∪ 𝐵 ⊆ 𝐴))
3		sseq2 3985	. . 3 ⊢ (𝐴 = 𝐵 → (∪ 𝐵 ⊆ 𝐴 ↔ ∪ 𝐵 ⊆ 𝐵))
4	2, 3	bitrd 279	. 2 ⊢ (𝐴 = 𝐵 → (∪ 𝐴 ⊆ 𝐴 ↔ ∪ 𝐵 ⊆ 𝐵))
5		df-tr 5230	. 2 ⊢ (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴)
6		df-tr 5230	. 2 ⊢ (Tr 𝐵 ↔ ∪ 𝐵 ⊆ 𝐵)
7	4, 5, 6	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ⊆ wss 3926  ∪ cuni 4883  Tr wtr 5229

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-ss 3943  df-uni 4884  df-tr 5230

This theorem is referenced by:  truni  5245  trint  5247  ordeq  6359  trcl  9742  tz9.1  9743  tz9.1c  9744  tctr  9754  tcmin  9755  tc2  9756  r1tr  9790  r1elssi  9819  tcrank  9898  iswun  10718  tskr1om2  10782  elgrug  10806  grutsk  10836  dfon2lem1  35801  dfon2lem3  35803  dfon2lem4  35804  dfon2lem5  35805  dfon2lem6  35806  dfon2lem7  35807  dfon2lem8  35808  dfon2  35810  dford3lem1  43050  dford3lem2  43051  nadd1rabtr  43412  wfaxext  45018  wfaxrep  45019  wfaxpow  45022  wfaxinf2  45026  wfac8prim  45027