Theorem treq 5218

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ⊆ wss 3896  ∪ cuni 4866  Tr wtr 5211

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3897  df-uni 4867  df-tr 5212

This theorem is used by:  truni  5227  trint  5229  ordeq  6372  trcl  9736  tz9.1  9737  tz9.1c  9738  tctr  9746  tcmin  9747  tc2  9748  r1tr  9790  r1elssi  9820  tcrank  9908  iswun  10796  tskhf  10860  elgrug  10884  grutsk  10914  trscott  35818  tz9.1regs  35870  dfon2lem1  36669  dfon2lem3  36671  dfon2lem4  36672  dfon2lem5  36673  dfon2lem6  36674  dfon2lem7  36675  dfon2lem8  36676  dfon2  36678  tz9.1tco  37395  dfttc3gw  37435  dford3lem1  44170  dford3lem2  44171  nadd1rabtr  44527  wfaxext  46119  wfaxrep  46120  wfaxpow  46123  wfaxinf2  46127  wfac8prim  46128