MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  trss Structured version   Unicode version

Theorem trss 4555
Description: An element of a transitive class is a subset of the class. (Contributed by NM, 7-Aug-1994.)
Assertion
Ref Expression
trss  |-  ( Tr  A  ->  ( B  e.  A  ->  B  C_  A ) )

Proof of Theorem trss
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 eleq1 2539 . . . . 5  |-  ( x  =  B  ->  (
x  e.  A  <->  B  e.  A ) )
2 sseq1 3530 . . . . 5  |-  ( x  =  B  ->  (
x  C_  A  <->  B  C_  A
) )
31, 2imbi12d 320 . . . 4  |-  ( x  =  B  ->  (
( x  e.  A  ->  x  C_  A )  <->  ( B  e.  A  ->  B  C_  A ) ) )
43imbi2d 316 . . 3  |-  ( x  =  B  ->  (
( Tr  A  -> 
( x  e.  A  ->  x  C_  A )
)  <->  ( Tr  A  ->  ( B  e.  A  ->  B  C_  A )
) ) )
5 dftr3 4550 . . . 4  |-  ( Tr  A  <->  A. x  e.  A  x  C_  A )
6 rsp 2833 . . . 4  |-  ( A. x  e.  A  x  C_  A  ->  ( x  e.  A  ->  x  C_  A ) )
75, 6sylbi 195 . . 3  |-  ( Tr  A  ->  ( x  e.  A  ->  x  C_  A ) )
84, 7vtoclg 3176 . 2  |-  ( B  e.  A  ->  ( Tr  A  ->  ( B  e.  A  ->  B  C_  A ) ) )
98pm2.43b 50 1  |-  ( Tr  A  ->  ( B  e.  A  ->  B  C_  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    e. wcel 1767   A.wral 2817    C_ wss 3481   Tr wtr 4546
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2822  df-v 3120  df-in 3488  df-ss 3495  df-uni 4252  df-tr 4547
This theorem is referenced by:  trin  4556  triun  4559  trint0  4563  tz7.2  4869  ordelss  4900  ordelord  4906  tz7.7  4910  trsucss  4969  tc2  8185  tcel  8188  r1ord3g  8209  r1ord2  8211  r1pwss  8214  rankwflemb  8223  r1elwf  8226  r1elssi  8235  uniwf  8249  itunitc1  8812  wunelss  9098  tskr1om2  9158  tskuni  9173  tskurn  9179  gruelss  9184  dfon2lem6  29154  dfon2lem9  29157  omsinds  29233  setindtr  30900  dford3lem1  30902  ordelordALT  32794  trsspwALT  33102  trsspwALT2  33103  trsspwALT3  33104  pwtrVD  33110  ordelordALTVD  33153
  Copyright terms: Public domain W3C validator