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

Theorem trss 4122
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 2343 . . . . 5  |-  ( x  =  B  ->  (
x  e.  A  <->  B  e.  A ) )
2 sseq1 3199 . . . . 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 4117 . . . 4  |-  ( Tr  A  <->  A. x  e.  A  x  C_  A )
6 rsp 2603 . . . 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 2843 . 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 1623    e. wcel 1684   A.wral 2543    C_ wss 3152   Tr wtr 4113
This theorem is referenced by:  trin  4123  triun  4126  trint0  4130  tz7.2  4377  ordelss  4408  ordelord  4414  tz7.7  4418  trsucss  4478  tc2  7427  tcel  7430  r1ord3g  7451  r1ord2  7453  r1pwss  7456  rankwflemb  7465  r1elwf  7468  r1elssi  7477  uniwf  7491  itunitc1  8046  wunelss  8330  tskr1om2  8390  tskuni  8405  tskurn  8411  gruelss  8416  dfon2lem6  23555  dfon2lem9  23558  omsinds  23630  imrestr  24510  ordsuccl3  24516  inttrp  24520  setindtr  26529  dford3lem1  26531  ordelordALT  27674  trsspwALT  27965  trsspwALT2  27966  trsspwALT3  27967  pwtrVD  27971  pwtrOLD  27972  ordelordALTVD  28016
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-v 2790  df-in 3159  df-ss 3166  df-uni 3828  df-tr 4114
  Copyright terms: Public domain W3C validator