Theorem treq 5214

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 4876	. . . 4 ⊢ (𝐴 = 𝐵 → ∪ 𝐴 = ∪ 𝐵)
2	1	sseq1d 3967	. . 3 ⊢ (𝐴 = 𝐵 → (∪ 𝐴 ⊆ 𝐴 ↔ ∪ 𝐵 ⊆ 𝐴))
3		sseq2 3962	. . 3 ⊢ (𝐴 = 𝐵 → (∪ 𝐵 ⊆ 𝐴 ↔ ∪ 𝐵 ⊆ 𝐵))
4	2, 3	bitrd 281	. 2 ⊢ (𝐴 = 𝐵 → (∪ 𝐴 ⊆ 𝐴 ↔ ∪ 𝐵 ⊆ 𝐵))
5		df-tr 5208	. 2 ⊢ (Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴)
6		df-tr 5208	. 2 ⊢ (Tr 𝐵 ↔ ∪ 𝐵 ⊆ 𝐵)
7	4, 5, 6	3bitr4g 316	1 ⊢ (𝐴 = 𝐵 → (Tr 𝐴 ↔ Tr 𝐵))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1560   ⊆ wss 3904  ∪ cuni 4865  Tr wtr 5207

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-ss 3921  df-uni 4866  df-tr 5208

This theorem is referenced by:  truni  5223  trint  5225  ordeq  6353  trcl  9683  tz9.1  9684  tz9.1c  9685  tctr  9693  tcmin  9694  tc2  9695  r1tr  9734  r1elssi  9763  tcrank  9842  iswun  10662  tskr1om2  10726  elgrug  10750  grutsk  10780  tz9.1regs  35430  dfon2lem1  36131  dfon2lem3  36133  dfon2lem4  36134  dfon2lem5  36135  dfon2lem6  36136  dfon2lem7  36137  dfon2lem8  36138  dfon2  36140  tz9.1tco  36843  dfttc3gw  36883  dford3lem1  43603  dford3lem2  43604  nadd1rabtr  43965  wfaxext  45569  wfaxrep  45570  wfaxpow  45573  wfaxinf2  45577  wfac8prim  45578