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

Theorem trss 4138
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 2356 . . . . 5  |-  ( x  =  B  ->  (
x  e.  A  <->  B  e.  A ) )
2 sseq1 3212 . . . . 5  |-  ( x  =  B  ->  (
x  C_  A  <->  B  C_  A
) )
31, 2imbi12d 311 . . . 4  |-  ( x  =  B  ->  (
( x  e.  A  ->  x  C_  A )  <->  ( B  e.  A  ->  B  C_  A ) ) )
43imbi2d 307 . . 3  |-  ( x  =  B  ->  (
( Tr  A  -> 
( x  e.  A  ->  x  C_  A )
)  <->  ( Tr  A  ->  ( B  e.  A  ->  B  C_  A )
) ) )
5 dftr3 4133 . . . 4  |-  ( Tr  A  <->  A. x  e.  A  x  C_  A )
6 rsp 2616 . . . 4  |-  ( A. x  e.  A  x  C_  A  ->  ( x  e.  A  ->  x  C_  A ) )
75, 6sylbi 187 . . 3  |-  ( Tr  A  ->  ( x  e.  A  ->  x  C_  A ) )
84, 7vtoclg 2856 . 2  |-  ( B  e.  A  ->  ( Tr  A  ->  ( B  e.  A  ->  B  C_  A ) ) )
98pm2.43b 46 1  |-  ( Tr  A  ->  ( B  e.  A  ->  B  C_  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    e. wcel 1696   A.wral 2556    C_ wss 3165   Tr wtr 4129
This theorem is referenced by:  trin  4139  triun  4142  trint0  4146  tz7.2  4393  ordelss  4424  ordelord  4430  tz7.7  4434  trsucss  4494  tc2  7443  tcel  7446  r1ord3g  7467  r1ord2  7469  r1pwss  7472  rankwflemb  7481  r1elwf  7484  r1elssi  7493  uniwf  7507  itunitc1  8062  wunelss  8346  tskr1om2  8406  tskuni  8421  tskurn  8427  gruelss  8432  dfon2lem6  24215  dfon2lem9  24218  omsinds  24290  imrestr  25201  ordsuccl3  25207  inttrp  25211  setindtr  27220  dford3lem1  27222  ordelordALT  28600  trsspwALT  28908  trsspwALT2  28909  trsspwALT3  28910  pwtrVD  28914  pwtrOLD  28915  ordelordALTVD  28959
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-v 2803  df-in 3172  df-ss 3179  df-uni 3844  df-tr 4130
  Copyright terms: Public domain W3C validator