Theorem treq 5219

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ⊆ wss 3899  ∪ cuni 4867  Tr wtr 5212

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-uni 4868  df-tr 5213

This theorem is used by:  truni  5228  trint  5230  ordeq  6369  trcl  9729  tz9.1  9730  tz9.1c  9731  tctr  9739  tcmin  9740  tc2  9741  r1tr  9783  r1elssi  9813  tcrank  9901  iswun  10789  tskhf  10853  elgrug  10877  grutsk  10907  tz9.1regs  35802  dfon2lem1  36545  dfon2lem3  36547  dfon2lem4  36548  dfon2lem5  36549  dfon2lem6  36550  dfon2lem7  36551  dfon2lem8  36552  dfon2  36554  tz9.1tco  37271  dfttc3gw  37311  dford3lem1  44032  dford3lem2  44033  nadd1rabtr  44389  wfaxext  45982  wfaxrep  45983  wfaxpow  45986  wfaxinf2  45990  wfac8prim  45991