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

Theorem relss 5734
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 3950 . 2 (𝐴𝐵 → (𝐵 ⊆ (V × V) → 𝐴 ⊆ (V × V)))
2 df-rel 5638 . 2 (Rel 𝐵𝐵 ⊆ (V × V))
3 df-rel 5638 . 2 (Rel 𝐴𝐴 ⊆ (V × V))
41, 2, 33imtr4g 296 1 (𝐴𝐵 → (Rel 𝐵 → Rel 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  Vcvv 3444  wss 3909   × cxp 5629  Rel wrel 5636
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3446  df-in 3916  df-ss 3926  df-rel 5638
This theorem is referenced by:  relin1  5765  relin2  5766  reldif  5768  relres  5963  iss  5986  cnvdif  6093  difxp  6113  sofld  6136  funss  6516  funssres  6541  fliftcnv  7251  fliftfun  7252  releldmdifi  7967  frxp  8047  reltpos  8130  swoer  8612  sbthcl  8973  fpwwe2lem8  10508  recmulnq  10834  prcdnq  10863  ltrel  11151  lerel  11153  dfle2  12995  dflt2  12996  isinv  17578  invsym2  17581  invfun  17582  oppcsect2  17597  oppcinv  17598  relfull  17730  relfth  17731  psss  18404  gicer  18999  gsum2d  19679  isunit  20010  txdis1cn  22909  hmpher  23058  tgphaus  23391  qustgplem  23395  tsmsxp  23429  xmeter  23709  ovoliunlem1  24789  taylf  25643  lgsquadlem1  26651  lgsquadlem2  26652  nvrel  29343  phrel  29556  bnrel  29608  hlrel  29631  gonan0  33760  frxp2  34180  frxp3  34186  sscoid  34394  trer  34684  fneer  34721  heicant  36009  iss2  36701  funALTVss  37057  disjss  37089  dvhopellsm  39476  diclspsn  39553  dih1dimatlem  39688
  Copyright terms: Public domain W3C validator