Theorem treq 5200

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ⊆ wss 3890  ∪ cuni 4851  Tr wtr 5193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-uni 4852  df-tr 5194

This theorem is referenced by:  truni  5209  trint  5211  ordeq  6325  trcl  9643  tz9.1  9644  tz9.1c  9645  tctr  9653  tcmin  9654  tc2  9655  r1tr  9694  r1elssi  9723  tcrank  9802  iswun  10621  tskr1om2  10685  elgrug  10709  grutsk  10739  tz9.1regs  35297  dfon2lem1  35982  dfon2lem3  35984  dfon2lem4  35985  dfon2lem5  35986  dfon2lem6  35987  dfon2lem7  35988  dfon2lem8  35989  dfon2  35991  tz9.1tco  36684  dfttc3gw  36724  dford3lem1  43475  dford3lem2  43476  nadd1rabtr  43837  wfaxext  45441  wfaxrep  45442  wfaxpow  45445  wfaxinf2  45449  wfac8prim  45450