Theorem treq 5186

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 4849	. . . 4 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
2	1	sseq1d 3946	. . 3 ⊢ (𝐴 = 𝐵 → (∪ 𝐴 ⊆ 𝐴 ↔ ∪ 𝐵 ⊆ 𝐴))
3		sseq2 3941	. . 3 ⊢ (𝐴 = 𝐵 → (∪ 𝐵 ⊆ 𝐴 ↔ ∪ 𝐵 ⊆ 𝐵))
4	2, 3	bitrd 280	. 2 ⊢ (𝐴 = 𝐵 → (∪ 𝐴 ⊆ 𝐴 ↔ ∪ 𝐵 ⊆ 𝐵))
5		df-tr 5180	. 2 ⊢ (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴)
6		df-tr 5180	. 2 ⊢ (Tr 𝐵 ↔ ∪ 𝐵 ⊆ 𝐵)
7	4, 5, 6	3bitr4g 315	1 ⊢ (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵))

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   ⊆ wss 3883  ∪ cuni 4838  Tr wtr 5179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-ss 3900  df-uni 4839  df-tr 5180

This theorem is referenced by:  truni  5195  trint  5197  ordeq  6317  trcl  9640  tz9.1  9641  tz9.1c  9642  tctr  9650  tcmin  9651  tc2  9652  r1tr  9691  r1elssi  9720  tcrank  9799  iswun  10618  tskr1om2  10682  elgrug  10706  grutsk  10736  tz9.1regs  35315  dfon2lem1  36009  dfon2lem3  36011  dfon2lem4  36012  dfon2lem5  36013  dfon2lem6  36014  dfon2lem7  36015  dfon2lem8  36016  dfon2  36018  tz9.1tco  36711  dfttc3gw  36751  dford3lem1  43471  dford3lem2  43472  nadd1rabtr  43833  wfaxext  45437  wfaxrep  45438  wfaxpow  45441  wfaxinf2  45445  wfac8prim  45446