Theorem treq 4503

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 4206	. . . 4 |- ( A = B -> U. A = U. B )
2	1	sseq1d 3459	. . 3 |- ( A = B -> ( U. A C_ A <-> U. B C_ A ) )
3		sseq2 3454	. . 3 |- ( A = B -> ( U. B C_ A <-> U. B C_ B ) )
4	2, 3	bitrd 257	. 2 |- ( A = B -> ( U. A C_ A <-> U. B C_ B ) )
5		df-tr 4498	. 2 |- ( Tr A <-> U. A C_ A )
6		df-tr 4498	. 2 |- ( Tr B <-> U. B C_ B )
7	4, 5, 6	3bitr4g 292	1 |- ( A = B -> ( Tr A <-> Tr B ) )

Syntax hints:   -> wi 4   <-> wb 188   = wceq 1444   C_ wss 3404   U.cuni 4198   Tr wtr 4497

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-rex 2743  df-in 3411  df-ss 3418  df-uni 4199  df-tr 4498

This theorem is referenced by:  truni  4511  ordeq  5430  trcl  8212  tz9.1  8213  tz9.1c  8214  tctr  8224  tcmin  8225  tc2  8226  r1tr  8247  r1elssi  8276  tcrank  8355  iswun  9129  tskr1om2  9193  elgrug  9217  grutsk  9247  dfon2lem1  30429  dfon2lem3  30431  dfon2lem4  30432  dfon2lem5  30433  dfon2lem6  30434  dfon2lem7  30435  dfon2lem8  30436  dfon2  30438  dford3lem1  35881  dford3lem2  35882