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

Theorem relss 4774
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 3187 . 2  |-  ( A 
C_  B  ->  ( B  C_  ( _V  X.  _V )  ->  A  C_  ( _V  X.  _V )
) )
2 df-rel 4695 . 2  |-  ( Rel 
B  <->  B  C_  ( _V 
X.  _V ) )
3 df-rel 4695 . 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 2789    C_ wss 3153    X. cxp 4686   Rel wrel 4693
This theorem is referenced by:  relin1  4802  relin2  4803  reldif  4804  relres  4982  iss  4997  cnvdif  5086  sofld  5120  funss  5239  funssres  5259  fliftcnv  5771  fliftfun  5772  difxp  6114  frxp  6186  reltpos  6200  tpostpos  6215  swoer  6683  erinxp  6728  sbthcl  6978  fpwwe2lem8  8254  fpwwe2lem9  8255  fpwwe2lem12  8258  recmulnq  8583  prcdnq  8612  ltrel  8882  lerel  8884  dfle2  10476  dflt2  10477  pwsle  13385  isinv  13656  invsym2  13659  invfun  13660  oppcsect2  13671  oppcinv  13672  relfull  13776  relfth  13777  psss  14317  gicer  14734  gsum2d  15217  isunit  15433  opsrtoslem2  16220  txdis1cn  17323  hmpher  17469  tgphaus  17793  divstgplem  17797  tsmsxp  17831  xmeter  17973  ovoliunlem1  18855  taylf  19734  lgsquadlem1  20587  lgsquadlem2  20588  nvrel  21150  phrel  21385  bnrel  21438  hlrel  21461  limptlimpr2lem2  24974  dualalg  25181  dualded  25182  trer  25626  fneer  25687  dvhopellsm  30574  diclspsn  30651  dih1dimatlem  30786
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-6 1707  ax-7 1712  ax-11 1719  ax-12 1869  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1534  df-nf 1537  df-sb 1636  df-clab 2271  df-cleq 2277  df-clel 2280  df-in 3160  df-ss 3167  df-rel 4695
  Copyright terms: Public domain W3C validator