Theorem treq 4536

Description: Equality theorem for the transitive class predicate. (Contributed by NM, 17-Sep-1993.)

Assertion

Ref	Expression
treq	|- ( A = B -> ( Tr A <-> Tr B ) )

Proof of Theorem treq

Step	Hyp	Ref	Expression
1		unieq 4242	. . . 4 |- ( A = B -> U. A = U. B )
2	1	sseq1d 3516	. . 3 |- ( A = B -> ( U. A C_ A <-> U. B C_ A ) )
3		sseq2 3511	. . 3 |- ( A = B -> ( U. B C_ A <-> U. B C_ B ) )
4	2, 3	bitrd 253	. 2 |- ( A = B -> ( U. A C_ A <-> U. B C_ B ) )
5		df-tr 4531	. 2 |- ( Tr A <-> U. A C_ A )
6		df-tr 4531	. 2 |- ( Tr B <-> U. B C_ B )
7	4, 5, 6	3bitr4g 288	1 |- ( A = B -> ( Tr A <-> Tr B ) )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1383   C_ wss 3461   U.cuni 4234   Tr wtr 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rex 2799  df-in 3468  df-ss 3475  df-uni 4235  df-tr 4531

This theorem is referenced by:  truni  4544  ordeq  4875  trcl  8162  tz9.1  8163  tz9.1c  8164  tctr  8174  tcmin  8175  tc2  8176  r1tr  8197  r1elssi  8226  tcrank  8305  iswun  9085  tskr1om2  9149  elgrug  9173  grutsk  9203  dfon2lem1  29191  dfon2lem3  29193  dfon2lem4  29194  dfon2lem5  29195  dfon2lem6  29196  dfon2lem7  29197  dfon2lem8  29198  dfon2  29200  dford3lem1  30944  dford3lem2  30945