Theorem treq 5219

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ⊆ wss 3899  ∪ cuni 4867  Tr wtr 5212

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 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3916  df-uni 4868  df-tr 5213

This theorem is used by:  truni  5228  trint  5230  ordeq  6364  trcl  9708  tz9.1  9709  tz9.1c  9710  tctr  9718  tcmin  9719  tc2  9720  r1tr  9759  r1elssi  9788  tcrank  9867  iswun  10714  tskr1om2  10778  elgrug  10802  grutsk  10832  tz9.1regs  35661  dfon2lem1  36361  dfon2lem3  36363  dfon2lem4  36364  dfon2lem5  36365  dfon2lem6  36366  dfon2lem7  36367  dfon2lem8  36368  dfon2  36370  tz9.1tco  37103  dfttc3gw  37143  dford3lem1  43868  dford3lem2  43869  nadd1rabtr  44230  wfaxext  45817  wfaxrep  45818  wfaxpow  45821  wfaxinf2  45825  wfac8prim  45826