Theorem treq 5229

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 4887	. . . 4 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
2	1	sseq1d 3976	. . 3 ⊢ (𝐴 = 𝐵 → (∪ 𝐴 ⊆ 𝐴 ↔ ∪ 𝐵 ⊆ 𝐴))
3		sseq2 3971	. . 3 ⊢ (𝐴 = 𝐵 → (∪ 𝐵 ⊆ 𝐴 ↔ ∪ 𝐵 ⊆ 𝐵))
4	2, 3	bitrd 282	. 2 ⊢ (𝐴 = 𝐵 → (∪ 𝐴 ⊆ 𝐴 ↔ ∪ 𝐵 ⊆ 𝐵))
5		df-tr 5223	. 2 ⊢ (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴)
6		df-tr 5223	. 2 ⊢ (Tr 𝐵 ↔ ∪ 𝐵 ⊆ 𝐵)
7	4, 5, 6	3bitr4g 317	1 ⊢ (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567   ⊆ wss 3913  ∪ cuni 4876  Tr wtr 5222

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-ss 3930  df-uni 4877  df-tr 5223

This theorem is referenced by:  truni  5238  trint  5240  ordeq  6368  trcl  9697  tz9.1  9698  tz9.1c  9699  tctr  9707  tcmin  9708  tc2  9709  r1tr  9748  r1elssi  9777  tcrank  9856  iswun  10689  tskr1om2  10753  elgrug  10777  grutsk  10807  tz9.1regs  35470  dfon2lem1  36172  dfon2lem3  36174  dfon2lem4  36175  dfon2lem5  36176  dfon2lem6  36177  dfon2lem7  36178  dfon2lem8  36179  dfon2  36181  tz9.1tco  36883  dfttc3gw  36923  dford3lem1  43645  dford3lem2  43646  nadd1rabtr  44007  wfaxext  45594  wfaxrep  45595  wfaxpow  45598  wfaxinf2  45602  wfac8prim  45603