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

Theorem relss 5624
 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 3925 . 2 (𝐴𝐵 → (𝐵 ⊆ (V × V) → 𝐴 ⊆ (V × V)))
2 df-rel 5530 . 2 (Rel 𝐵𝐵 ⊆ (V × V))
3 df-rel 5530 . 2 (Rel 𝐴𝐴 ⊆ (V × V))
41, 2, 33imtr4g 299 1 (𝐴𝐵 → (Rel 𝐵 → Rel 𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4  Vcvv 3444   ⊆ wss 3884   × cxp 5521  Rel wrel 5528 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-in 3891  df-ss 3901  df-rel 5530 This theorem is referenced by:  relin1  5653  relin2  5654  reldif  5656  relres  5851  iss  5874  cnvdif  5973  difxp  5992  sofld  6015  funss  6347  funssres  6372  fliftcnv  7047  fliftfun  7048  releldmdifi  7730  frxp  7807  reltpos  7884  swoer  8306  sbthcl  8627  fpwwe2lem9  10053  recmulnq  10379  prcdnq  10408  ltrel  10696  lerel  10698  dfle2  12532  dflt2  12533  isinv  17026  invsym2  17029  invfun  17030  oppcsect2  17045  oppcinv  17046  relfull  17174  relfth  17175  psss  17820  gicer  18412  gsum2d  19089  isunit  19407  txdis1cn  22244  hmpher  22393  tgphaus  22726  qustgplem  22730  tsmsxp  22764  xmeter  23044  ovoliunlem1  24110  taylf  24960  lgsquadlem1  25968  lgsquadlem2  25969  nvrel  28389  phrel  28602  bnrel  28654  hlrel  28677  gonan0  32753  sscoid  33488  trer  33778  fneer  33815  heicant  35091  iss2  35760  funALTVss  36091  disjss  36123  dvhopellsm  38412  diclspsn  38489  dih1dimatlem  38624
 Copyright terms: Public domain W3C validator