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

Theorem relss 5787
Description: Subclass theorem for relation predicate. Theorem 2 of [Suppes] p. 58. (Contributed by NM, 15-Aug-1994.)
Assertion
Ref Expression
relss (𝐴𝐵 → (Rel 𝐵 → Rel 𝐴))

Proof of Theorem relss
StepHypRef Expression
1 sstr2 3986 . 2 (𝐴𝐵 → (𝐵 ⊆ (V × V) → 𝐴 ⊆ (V × V)))
2 df-rel 5689 . 2 (Rel 𝐵𝐵 ⊆ (V × V))
3 df-rel 5689 . 2 (Rel 𝐴𝐴 ⊆ (V × V))
41, 2, 33imtr4g 295 1 (𝐴𝐵 → (Rel 𝐵 → Rel 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  Vcvv 3462  wss 3947   × cxp 5680  Rel wrel 5687
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804
This theorem depends on definitions:  df-bi 206  df-ss 3964  df-rel 5689
This theorem is referenced by:  relin1  5818  relin2  5819  reldif  5821  relres  6015  iss  6044  cnvdif  6155  difxp  6175  sofld  6198  funss  6578  funssres  6603  fliftcnv  7323  fliftfun  7324  releldmdifi  8059  frxp  8140  frxp2  8158  frxp3  8165  reltpos  8246  swoer  8765  sbthcl  9133  fpwwe2lem8  10681  recmulnq  11007  prcdnq  11036  ltrel  11326  lerel  11328  dfle2  13180  dflt2  13181  isinv  17776  invsym2  17779  invfun  17780  oppcsect2  17795  oppcinv  17796  relfull  17930  relfth  17931  psss  18605  gicer  19271  gsum2d  19970  isunit  20355  txdis1cn  23630  hmpher  23779  tgphaus  24112  qustgplem  24116  tsmsxp  24150  xmeter  24430  ovoliunlem1  25522  taylf  26388  lgsquadlem1  27409  lgsquadlem2  27410  noseqrdgfn  28280  nvrel  30535  phrel  30748  bnrel  30800  hlrel  30823  gonan0  35220  sscoid  35737  trer  36028  fneer  36065  heicant  37356  iss2  38042  funALTVss  38397  disjss  38429  dvhopellsm  40816  diclspsn  40893  dih1dimatlem  41028  gricrel  47467  grlicrel  47496
  Copyright terms: Public domain W3C validator