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

Theorem relss 4896
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 3291 . 2  |-  ( A 
C_  B  ->  ( B  C_  ( _V  X.  _V )  ->  A  C_  ( _V  X.  _V )
) )
2 df-rel 4818 . 2  |-  ( Rel 
B  <->  B  C_  ( _V 
X.  _V ) )
3 df-rel 4818 . 2  |-  ( Rel 
A  <->  A  C_  ( _V 
X.  _V ) )
41, 2, 33imtr4g 262 1  |-  ( A 
C_  B  ->  ( Rel  B  ->  Rel  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   _Vcvv 2892    C_ wss 3256    X. cxp 4809   Rel wrel 4816
This theorem is referenced by:  relin1  4925  relin2  4926  reldif  4927  relres  5107  iss  5122  cnvdif  5211  sofld  5251  funss  5405  funssres  5426  fliftcnv  5965  fliftfun  5966  difxp  6312  frxp  6385  reltpos  6413  tpostpos  6428  swoer  6862  erinxp  6907  sbthcl  7158  fpwwe2lem8  8438  fpwwe2lem9  8439  fpwwe2lem12  8442  recmulnq  8767  prcdnq  8796  ltrel  9066  lerel  9068  dfle2  10665  dflt2  10666  pwsle  13634  isinv  13905  invsym2  13908  invfun  13909  oppcsect2  13920  oppcinv  13921  relfull  14025  relfth  14026  psss  14566  gicer  14983  gsum2d  15466  isunit  15682  opsrtoslem2  16465  txdis1cn  17581  hmpher  17730  tgphaus  18060  divstgplem  18064  tsmsxp  18098  xmeter  18346  ovoliunlem1  19258  taylf  20137  lgsquadlem1  20998  lgsquadlem2  20999  nvrel  21922  phrel  22157  bnrel  22210  hlrel  22233  elrn3  25137  dffun10  25470  trer  26003  fneer  26052  dvhopellsm  31283  diclspsn  31360  dih1dimatlem  31495
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-in 3263  df-ss 3270  df-rel 4818
  Copyright terms: Public domain W3C validator