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  12996  dflt2  12997  isinv  17579  invsym2  17582  invfun  17583  oppcsect2  17598  oppcinv  17599  relfull  17731  relfth  17732  psss  18405  gicer  19001  gsum2d  19684  isunit  20015  txdis1cn  22914  hmpher  23063  tgphaus  23396  qustgplem  23400  tsmsxp  23434  xmeter  23714  ovoliunlem1  24794  taylf  25648  lgsquadlem1  26656  lgsquadlem2  26657  nvrel  29349  phrel  29562  bnrel  29614  hlrel  29637  gonan0  33766  frxp2  34183  frxp3  34189  sscoid  34429  trer  34719  fneer  34756  heicant  36044  iss2  36736  funALTVss  37092  disjss  37124  dvhopellsm  39511  diclspsn  39588  dih1dimatlem  39723
  Copyright terms: Public domain W3C validator