Theorem treq 4538

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 4243	. . . 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 4533	. 2 |- ( Tr A <-> U. A C_ A )
6		df-tr 4533	. 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 1398   C_ wss 3461   U.cuni 4235   Tr wtr 4532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rex 2810  df-in 3468  df-ss 3475  df-uni 4236  df-tr 4533

This theorem is referenced by:  truni  4546  ordeq  4874  trcl  8150  tz9.1  8151  tz9.1c  8152  tctr  8162  tcmin  8163  tc2  8164  r1tr  8185  r1elssi  8214  tcrank  8293  iswun  9071  tskr1om2  9135  elgrug  9159  grutsk  9189  dfon2lem1  29458  dfon2lem3  29460  dfon2lem4  29461  dfon2lem5  29462  dfon2lem6  29463  dfon2lem7  29464  dfon2lem8  29465  dfon2  29467  dford3lem1  31210  dford3lem2  31211