Theorem treq 5227

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ⊆ wss 3906  ∪ cuni 4874  Tr wtr 5220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3923  df-uni 4875  df-tr 5221

This theorem is used by:  truni  5236  trint  5238  ordeq  6371  trcl  9704  tz9.1  9705  tz9.1c  9706  tctr  9714  tcmin  9715  tc2  9716  r1tr  9755  r1elssi  9784  tcrank  9863  iswun  10706  tskr1om2  10770  elgrug  10794  grutsk  10824  tz9.1regs  35606  dfon2lem1  36312  dfon2lem3  36314  dfon2lem4  36315  dfon2lem5  36316  dfon2lem6  36317  dfon2lem7  36318  dfon2lem8  36319  dfon2  36321  tz9.1tco  37053  dfttc3gw  37093  dford3lem1  43813  dford3lem2  43814  nadd1rabtr  44175  wfaxext  45762  wfaxrep  45763  wfaxpow  45766  wfaxinf2  45770  wfac8prim  45771