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

Theorem relss 4728
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 3128 . 2  |-  ( A 
C_  B  ->  ( B  C_  ( _V  X.  _V )  ->  A  C_  ( _V  X.  _V )
) )
2 df-rel 4641 . 2  |-  ( Rel 
B  <->  B  C_  ( _V 
X.  _V ) )
3 df-rel 4641 . 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 2740    C_ wss 3094    X. cxp 4624   Rel wrel 4631
This theorem is referenced by:  relin1  4756  relin2  4757  reldif  4758  relres  4936  iss  4951  cnvdif  5040  sofld  5074  funss  5177  funssres  5197  fliftcnv  5709  fliftfun  5710  difxp  6052  frxp  6124  reltpos  6138  tpostpos  6153  swoer  6621  erinxp  6666  sbthcl  6916  fpwwe2lem8  8192  fpwwe2lem9  8193  fpwwe2lem12  8196  recmulnq  8521  prcdnq  8550  ltrel  8820  lerel  8822  dfle2  10413  dflt2  10414  pwsle  13318  isinv  13589  invsym2  13592  invfun  13593  oppcsect2  13604  oppcinv  13605  relfull  13709  relfth  13710  psss  14250  gicer  14667  gsum2d  15150  isunit  15366  opsrtoslem2  16153  txdis1cn  17256  hmpher  17402  tgphaus  17726  divstgplem  17730  tsmsxp  17764  xmeter  17906  ovoliunlem1  18788  taylf  19667  lgsquadlem1  20520  lgsquadlem2  20521  nvrel  21083  phrel  21318  bnrel  21371  hlrel  21394  limptlimpr2lem2  24907  dualalg  25114  dualded  25115  trer  25559  fneer  25620  dvhopellsm  30437  diclspsn  30514  dih1dimatlem  30649
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 3101  df-ss 3108  df-rel 4641
  Copyright terms: Public domain W3C validator