ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  relss Unicode version

Theorem relss 4727
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 3176 . 2  |-  ( A 
C_  B  ->  ( B  C_  ( _V  X.  _V )  ->  A  C_  ( _V  X.  _V )
) )
2 df-rel 4647 . 2  |-  ( Rel 
B  <->  B  C_  ( _V 
X.  _V ) )
3 df-rel 4647 . 2  |-  ( Rel 
A  <->  A  C_  ( _V 
X.  _V ) )
41, 2, 33imtr4g 205 1  |-  ( A 
C_  B  ->  ( Rel  B  ->  Rel  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   _Vcvv 2751    C_ wss 3143    X. cxp 4638   Rel wrel 4645
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-11 1516  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2170
This theorem depends on definitions:  df-bi 117  df-nf 1471  df-sb 1773  df-clab 2175  df-cleq 2181  df-clel 2184  df-in 3149  df-ss 3156  df-rel 4647
This theorem is referenced by:  relin1  4758  relin2  4759  reldif  4760  relres  4949  iss  4967  cnvdif  5049  funss  5249  funssres  5272  fliftcnv  5811  fliftfun  5812  reltpos  6268  tpostpos  6282  swoer  6580  erinxp  6626  ltrel  8036  lerel  8038  txdis1cn  14161  xmeter  14319
  Copyright terms: Public domain W3C validator