Theorem treq 5225

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ⊆ wss 3900  ∪ cuni 4872  Tr wtr 5218

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-uni 4873  df-tr 5219

This theorem is used by:  truni  5234  trint  5236  ordeq  6395  trcl  9766  tz9.1  9767  tz9.1c  9768  tctr  9776  tcmin  9777  tc2  9778  r1tr  9820  r1elssi  9850  tcrank  9938  iswun  10828  tskhf  10892  elgrug  10916  grutsk  10946  trscott  35883  tz9.1regs  35943  dfon2lem1  36760  dfon2lem3  36762  dfon2lem4  36763  dfon2lem5  36764  dfon2lem6  36765  dfon2lem7  36766  dfon2lem8  36767  dfon2  36769  tz9.1tco  37486  dfttc3gw  37526  dford3lem1  44299  dford3lem2  44300  nadd1rabtr  44651  wfaxext  46247  wfaxrep  46248  wfaxpow  46251  wfaxinf2  46255  wfac8prim  46256