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

Theorem trss 4313
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 2498 . . . . 5  |-  ( x  =  B  ->  (
x  e.  A  <->  B  e.  A ) )
2 sseq1 3371 . . . . 5  |-  ( x  =  B  ->  (
x  C_  A  <->  B  C_  A
) )
31, 2imbi12d 313 . . . 4  |-  ( x  =  B  ->  (
( x  e.  A  ->  x  C_  A )  <->  ( B  e.  A  ->  B  C_  A ) ) )
43imbi2d 309 . . 3  |-  ( x  =  B  ->  (
( Tr  A  -> 
( x  e.  A  ->  x  C_  A )
)  <->  ( Tr  A  ->  ( B  e.  A  ->  B  C_  A )
) ) )
5 dftr3 4308 . . . 4  |-  ( Tr  A  <->  A. x  e.  A  x  C_  A )
6 rsp 2768 . . . 4  |-  ( A. x  e.  A  x  C_  A  ->  ( x  e.  A  ->  x  C_  A ) )
75, 6sylbi 189 . . 3  |-  ( Tr  A  ->  ( x  e.  A  ->  x  C_  A ) )
84, 7vtoclg 3013 . 2  |-  ( B  e.  A  ->  ( Tr  A  ->  ( B  e.  A  ->  B  C_  A ) ) )
98pm2.43b 49 1  |-  ( Tr  A  ->  ( B  e.  A  ->  B  C_  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    e. wcel 1726   A.wral 2707    C_ wss 3322   Tr wtr 4304
This theorem is referenced by:  trin  4314  triun  4317  trint0  4321  tz7.2  4568  ordelss  4599  ordelord  4605  tz7.7  4609  trsucss  4669  tc2  7683  tcel  7686  r1ord3g  7707  r1ord2  7709  r1pwss  7712  rankwflemb  7721  r1elwf  7724  r1elssi  7733  uniwf  7747  itunitc1  8302  wunelss  8585  tskr1om2  8645  tskuni  8660  tskurn  8666  gruelss  8671  dfon2lem6  25417  dfon2lem9  25420  omsinds  25496  setindtr  27097  dford3lem1  27099  ordelordALT  28684  trsspwALT  28993  trsspwALT2  28994  trsspwALT3  28995  pwtrVD  28999  ordelordALTVD  29041
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2712  df-v 2960  df-in 3329  df-ss 3336  df-uni 4018  df-tr 4305
  Copyright terms: Public domain W3C validator