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

Theorem relss 4749
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 3147 . 2  |-  ( A 
C_  B  ->  ( B  C_  ( _V  X.  _V )  ->  A  C_  ( _V  X.  _V )
) )
2 df-rel 4662 . 2  |-  ( Rel 
B  <->  B  C_  ( _V 
X.  _V ) )
3 df-rel 4662 . 2  |-  ( Rel 
A  <->  A  C_  ( _V 
X.  _V ) )
41, 2, 33imtr4g 263 1  |-  ( A 
C_  B  ->  ( Rel  B  ->  Rel  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6   _Vcvv 2757    C_ wss 3113    X. cxp 4645   Rel wrel 4652
This theorem is referenced by:  relin1  4777  relin2  4778  reldif  4779  relres  4957  iss  4972  cnvdif  5061  sofld  5095  funss  5198  funssres  5218  fliftcnv  5730  fliftfun  5731  difxp  6073  frxp  6145  reltpos  6159  tpostpos  6174  swoer  6642  erinxp  6687  sbthcl  6937  fpwwe2lem8  8213  fpwwe2lem9  8214  fpwwe2lem12  8217  recmulnq  8542  prcdnq  8571  ltrel  8841  lerel  8843  dfle2  10434  dflt2  10435  pwsle  13339  isinv  13610  invsym2  13613  invfun  13614  oppcsect2  13625  oppcinv  13626  relfull  13730  relfth  13731  psss  14271  gicer  14688  gsum2d  15171  isunit  15387  opsrtoslem2  16174  txdis1cn  17277  hmpher  17423  tgphaus  17747  divstgplem  17751  tsmsxp  17785  xmeter  17927  ovoliunlem1  18809  taylf  19688  lgsquadlem1  20541  lgsquadlem2  20542  nvrel  21104  phrel  21339  bnrel  21392  hlrel  21415  limptlimpr2lem2  24928  dualalg  25135  dualded  25136  trer  25580  fneer  25641  dvhopellsm  30458  diclspsn  30535  dih1dimatlem  30670
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-in 3120  df-ss 3127  df-rel 4662
  Copyright terms: Public domain W3C validator