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

Theorem relss 4682
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 3107 . 2  |-  ( A 
C_  B  ->  ( B  C_  ( _V  X.  _V )  ->  A  C_  ( _V  X.  _V )
) )
2 df-rel 4595 . 2  |-  ( Rel 
B  <->  B  C_  ( _V 
X.  _V ) )
3 df-rel 4595 . 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 2727    C_ wss 3078    X. cxp 4578   Rel wrel 4585
This theorem is referenced by:  relin1  4710  relin2  4711  reldif  4712  relres  4890  iss  4905  cnvdif  4994  sofld  5028  funss  5131  funssres  5151  fliftcnv  5662  fliftfun  5663  difxp  6005  frxp  6077  reltpos  6091  tpostpos  6106  swoer  6574  erinxp  6619  sbthcl  6868  fpwwe2lem8  8139  fpwwe2lem9  8140  fpwwe2lem12  8143  recmulnq  8468  prcdnq  8497  ltrel  8767  lerel  8769  dfle2  10360  dflt2  10361  pwsle  13265  isinv  13506  invsym2  13509  invfun  13510  oppcsect2  13521  oppcinv  13522  relfull  13626  relfth  13627  psss  14158  gicer  14575  gsum2d  15058  isunit  15274  opsrtoslem2  16058  txdis1cn  17161  hmpher  17307  tgphaus  17631  divstgplem  17635  tsmsxp  17669  xmeter  17811  ovoliunlem1  18693  taylf  19572  lgsquadlem1  20425  lgsquadlem2  20426  nvrel  20988  phrel  21223  bnrel  21276  hlrel  21299  limptlimpr2lem2  24741  dualalg  24948  dualded  24949  trer  25393  fneer  25454  dvhopellsm  29996  diclspsn  30073  dih1dimatlem  30208
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 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-in 3085  df-ss 3089  df-rel 4595
  Copyright terms: Public domain W3C validator