Theorem treq 4551

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

Assertion

Ref	Expression
treq

Proof of Theorem treq

Step	Hyp	Ref	Expression
1		unieq 4257	. . . 4
2	1	sseq1d 3530	. . 3
3		sseq2 3525	. . 3
4	2, 3	bitrd 253	. 2
5		df-tr 4546	. 2
6		df-tr 4546	. 2
7	4, 5, 6	3bitr4g 288	1

Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  C_wss 3475  U.cuni 4249  Trwtr 4545

This theorem is referenced by:  truni  4559  ordeq  4890  trcl  8180  tz9.1  8181  tz9.1c  8182  tctr  8192  tcmin  8193  tc2  8194  r1tr  8215  r1elssi  8244  tcrank  8323  iswun  9103  tskr1om2  9167  elgrug  9191  grutsk  9221  dfon2lem1  29215  dfon2lem3  29217  dfon2lem4  29218  dfon2lem5  29219  dfon2lem6  29220  dfon2lem7  29221  dfon2lem8  29222  dfon2  29224  dford3lem1  30968  dford3lem2  30969

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-in 3482  df-ss 3489  df-uni 4250  df-tr 4546