Theorem trss 4554

Description: An element of a transitive class is a subset of the class. (Contributed by NM, 7-Aug-1994.)

Assertion

Ref	Expression
trss

Proof of Theorem trss

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1 2529	. . . . 5
2		sseq1 3524	. . . . 5
3	1, 2	imbi12d 320	. . . 4
4	3	imbi2d 316	. . 3
5		dftr3 4549	. . . 4
6		rsp 2823	. . . 4
7	5, 6	sylbi 195	. . 3
8	4, 7	vtoclg 3167	. 2
9	8	pm2.43b 50	1

Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818  A.wral 2807  C_wss 3475  Trwtr 4545

This theorem is referenced by:  trin  4555  triun  4558  trint0  4562  tz7.2  4868  ordelss  4899  ordelord  4905  tz7.7  4909  trsucss  4968  tc2  8194  tcel  8197  r1ord3g  8218  r1ord2  8220  r1pwss  8223  rankwflemb  8232  r1elwf  8235  r1elssi  8244  uniwf  8258  itunitc1  8821  wunelss  9107  tskr1om2  9167  tskuni  9182  tskurn  9188  gruelss  9193  dfon2lem6  29220  dfon2lem9  29223  omsinds  29299  setindtr  30966  dford3lem1  30968  ordelordALT  33308  trsspwALT  33616  trsspwALT2  33617  trsspwALT3  33618  pwtrVD  33624  ordelordALTVD  33667

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-ral 2812  df-v 3111  df-in 3482  df-ss 3489  df-uni 4250  df-tr 4546