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

Theorem relss 4791
Description: Subclass theorem for relation predicate. Theorem 2 of [Suppes] p. 58. (Contributed by NM, 15-Aug-1994.)
Assertion
Ref Expression
relss  |-  ( A 
C_  B  ->  ( Rel  B  ->  Rel  A ) )

Proof of Theorem relss
StepHypRef Expression
1 sstr2 3199 . 2  |-  ( A 
C_  B  ->  ( B  C_  ( _V  X.  _V )  ->  A  C_  ( _V  X.  _V )
) )
2 df-rel 4712 . 2  |-  ( Rel 
B  <->  B  C_  ( _V 
X.  _V ) )
3 df-rel 4712 . 2  |-  ( Rel 
A  <->  A  C_  ( _V 
X.  _V ) )
41, 2, 33imtr4g 261 1  |-  ( A 
C_  B  ->  ( Rel  B  ->  Rel  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   _Vcvv 2801    C_ wss 3165    X. cxp 4703   Rel wrel 4710
This theorem is referenced by:  relin1  4819  relin2  4820  reldif  4821  relres  4999  iss  5014  cnvdif  5103  sofld  5137  funss  5289  funssres  5310  fliftcnv  5826  fliftfun  5827  difxp  6169  frxp  6241  reltpos  6255  tpostpos  6270  swoer  6704  erinxp  6749  sbthcl  6999  fpwwe2lem8  8275  fpwwe2lem9  8276  fpwwe2lem12  8279  recmulnq  8604  prcdnq  8633  ltrel  8903  lerel  8905  dfle2  10497  dflt2  10498  pwsle  13407  isinv  13678  invsym2  13681  invfun  13682  oppcsect2  13693  oppcinv  13694  relfull  13798  relfth  13799  psss  14339  gicer  14756  gsum2d  15239  isunit  15455  opsrtoslem2  16242  txdis1cn  17345  hmpher  17491  tgphaus  17815  divstgplem  17819  tsmsxp  17853  xmeter  17995  ovoliunlem1  18877  taylf  19756  lgsquadlem1  20609  lgsquadlem2  20610  nvrel  21174  phrel  21409  bnrel  21462  hlrel  21485  elrn3  24191  dffun10  24524  limptlimpr2lem2  25678  dualalg  25885  dualded  25886  trer  26330  fneer  26391  dvhopellsm  31929  diclspsn  32006  dih1dimatlem  32141
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-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179  df-rel 4712
  Copyright terms: Public domain W3C validator