Theorem treq 4758

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 4444	. . . 4 |- ( A = B -> U. A = U. B )
2	1	sseq1d 3632	. . 3 |- ( A = B -> ( U. A C_ A <-> U. B C_ A ) )
3		sseq2 3627	. . 3 |- ( A = B -> ( U. B C_ A <-> U. B C_ B ) )
4	2, 3	bitrd 268	. 2 |- ( A = B -> ( U. A C_ A <-> U. B C_ B ) )
5		df-tr 4753	. 2 |- ( Tr A <-> U. A C_ A )
6		df-tr 4753	. 2 |- ( Tr B <-> U. B C_ B )
7	4, 5, 6	3bitr4g 303	1 |- ( A = B -> ( Tr A <-> Tr B ) )

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   C_ wss 3574   U.cuni 4436   Tr wtr 4752

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-in 3581  df-ss 3588  df-uni 4437  df-tr 4753

This theorem is referenced by:  truni  4767  ordeq  5730  trcl  8604  tz9.1  8605  tz9.1c  8606  tctr  8616  tcmin  8617  tc2  8618  r1tr  8639  r1elssi  8668  tcrank  8747  iswun  9526  tskr1om2  9590  elgrug  9614  grutsk  9644  dfon2lem1  31688  dfon2lem3  31690  dfon2lem4  31691  dfon2lem5  31692  dfon2lem6  31693  dfon2lem7  31694  dfon2lem8  31695  dfon2  31697  dford3lem1  37593  dford3lem2  37594