Theorem treq 5203

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ⊆ wss 3897  ∪ cuni 4856  Tr wtr 5196

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3914  df-uni 4857  df-tr 5197

This theorem is referenced by:  truni  5211  trint  5213  ordeq  6313  trcl  9618  tz9.1  9619  tz9.1c  9620  tctr  9628  tcmin  9629  tc2  9630  r1tr  9669  r1elssi  9698  tcrank  9777  iswun  10595  tskr1om2  10659  elgrug  10683  grutsk  10713  tz9.1regs  35130  dfon2lem1  35825  dfon2lem3  35827  dfon2lem4  35828  dfon2lem5  35829  dfon2lem6  35830  dfon2lem7  35831  dfon2lem8  35832  dfon2  35834  dford3lem1  43129  dford3lem2  43130  nadd1rabtr  43491  wfaxext  45096  wfaxrep  45097  wfaxpow  45100  wfaxinf2  45104  wfac8prim  45105