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

Theorem relss 4926
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 3319 . 2  |-  ( A 
C_  B  ->  ( B  C_  ( _V  X.  _V )  ->  A  C_  ( _V  X.  _V )
) )
2 df-rel 4848 . 2  |-  ( Rel 
B  <->  B  C_  ( _V 
X.  _V ) )
3 df-rel 4848 . 2  |-  ( Rel 
A  <->  A  C_  ( _V 
X.  _V ) )
41, 2, 33imtr4g 262 1  |-  ( A 
C_  B  ->  ( Rel  B  ->  Rel  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   _Vcvv 2920    C_ wss 3284    X. cxp 4839   Rel wrel 4846
This theorem is referenced by:  relin1  4955  relin2  4956  reldif  4957  relres  5137  iss  5152  cnvdif  5241  sofld  5281  funss  5435  funssres  5456  fliftcnv  5996  fliftfun  5997  difxp  6343  frxp  6419  reltpos  6447  tpostpos  6462  swoer  6896  erinxp  6941  sbthcl  7192  fpwwe2lem8  8472  fpwwe2lem9  8473  fpwwe2lem12  8476  recmulnq  8801  prcdnq  8830  ltrel  9100  lerel  9102  dfle2  10700  dflt2  10701  pwsle  13673  isinv  13944  invsym2  13947  invfun  13948  oppcsect2  13959  oppcinv  13960  relfull  14064  relfth  14065  psss  14605  gicer  15022  gsum2d  15505  isunit  15721  opsrtoslem2  16504  txdis1cn  17624  hmpher  17773  tgphaus  18103  divstgplem  18107  tsmsxp  18141  xmeter  18420  ovoliunlem1  19355  taylf  20234  lgsquadlem1  21095  lgsquadlem2  21096  nvrel  22038  phrel  22273  bnrel  22326  hlrel  22349  elrn3  25338  dffun10  25671  trer  26213  fneer  26262  dvhopellsm  31604  diclspsn  31681  dih1dimatlem  31816
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2395  df-cleq 2401  df-clel 2404  df-in 3291  df-ss 3298  df-rel 4848
  Copyright terms: Public domain W3C validator