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

Theorem trss 4497
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 2474 . . . . 5  |-  ( x  =  B  ->  (
x  e.  A  <->  B  e.  A ) )
2 sseq1 3462 . . . . 5  |-  ( x  =  B  ->  (
x  C_  A  <->  B  C_  A
) )
31, 2imbi12d 318 . . . 4  |-  ( x  =  B  ->  (
( x  e.  A  ->  x  C_  A )  <->  ( B  e.  A  ->  B  C_  A ) ) )
43imbi2d 314 . . 3  |-  ( x  =  B  ->  (
( Tr  A  -> 
( x  e.  A  ->  x  C_  A )
)  <->  ( Tr  A  ->  ( B  e.  A  ->  B  C_  A )
) ) )
5 dftr3 4492 . . . 4  |-  ( Tr  A  <->  A. x  e.  A  x  C_  A )
6 rsp 2769 . . . 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 3116 . 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 setvar class
Syntax hints:    -> wi 4    = wceq 1405    e. wcel 1842   A.wral 2753    C_ wss 3413   Tr wtr 4488
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ral 2758  df-v 3060  df-in 3420  df-ss 3427  df-uni 4191  df-tr 4489
This theorem is referenced by:  trin  4498  triun  4501  trint0  4505  tz7.2  4806  ordelss  5425  ordelord  5431  tz7.7  5435  trsucss  5494  omsinds  6701  tc2  8204  tcel  8207  r1ord3g  8228  r1ord2  8230  r1pwss  8233  rankwflemb  8242  r1elwf  8245  r1elssi  8254  uniwf  8268  itunitc1  8831  wunelss  9115  tskr1om2  9175  tskuni  9190  tskurn  9196  gruelss  9201  dfon2lem6  29994  dfon2lem9  29997  setindtr  35308  dford3lem1  35310  ordelordALT  36308  trsspwALT  36620  trsspwALT2  36621  trsspwALT3  36622  pwtrVD  36634  ordelordALTVD  36678
  Copyright terms: Public domain W3C validator