Theorem treq 5225

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570   ⊆ wss 3905  ∪ cuni 4872  Tr wtr 5218

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3922  df-uni 4873  df-tr 5219

This theorem is referenced by:  truni  5234  trint  5236  ordeq  6367  trcl  9693  tz9.1  9694  tz9.1c  9695  tctr  9703  tcmin  9704  tc2  9705  r1tr  9744  r1elssi  9773  tcrank  9852  iswun  10684  tskr1om2  10748  elgrug  10772  grutsk  10802  tz9.1regs  35547  dfon2lem1  36273  dfon2lem3  36275  dfon2lem4  36276  dfon2lem5  36277  dfon2lem6  36278  dfon2lem7  36279  dfon2lem8  36280  dfon2  36282  tz9.1tco  37014  dfttc3gw  37054  dford3lem1  43773  dford3lem2  43774  nadd1rabtr  44135  wfaxext  45722  wfaxrep  45723  wfaxpow  45726  wfaxinf2  45730  wfac8prim  45731