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

Theorem relss 4775
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 3186 . 2  |-  ( A 
C_  B  ->  ( B  C_  ( _V  X.  _V )  ->  A  C_  ( _V  X.  _V )
) )
2 df-rel 4696 . 2  |-  ( Rel 
B  <->  B  C_  ( _V 
X.  _V ) )
3 df-rel 4696 . 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 2788    C_ wss 3152    X. cxp 4687   Rel wrel 4694
This theorem is referenced by:  relin1  4803  relin2  4804  reldif  4805  relres  4983  iss  4998  cnvdif  5087  sofld  5121  funss  5273  funssres  5294  fliftcnv  5810  fliftfun  5811  difxp  6153  frxp  6225  reltpos  6239  tpostpos  6254  swoer  6688  erinxp  6733  sbthcl  6983  fpwwe2lem8  8259  fpwwe2lem9  8260  fpwwe2lem12  8263  recmulnq  8588  prcdnq  8617  ltrel  8887  lerel  8889  dfle2  10481  dflt2  10482  pwsle  13391  isinv  13662  invsym2  13665  invfun  13666  oppcsect2  13677  oppcinv  13678  relfull  13782  relfth  13783  psss  14323  gicer  14740  gsum2d  15223  isunit  15439  opsrtoslem2  16226  txdis1cn  17329  hmpher  17475  tgphaus  17799  divstgplem  17803  tsmsxp  17837  xmeter  17979  ovoliunlem1  18861  taylf  19740  lgsquadlem1  20593  lgsquadlem2  20594  nvrel  21158  phrel  21393  bnrel  21446  hlrel  21469  elrn3  24120  dffun10  24453  limptlimpr2lem2  25575  dualalg  25782  dualded  25783  trer  26227  fneer  26288  dvhopellsm  31307  diclspsn  31384  dih1dimatlem  31519
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-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166  df-rel 4696
  Copyright terms: Public domain W3C validator