Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  relss GIF version

Theorem relss 4594
 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 3072 . 2 (𝐴𝐵 → (𝐵 ⊆ (V × V) → 𝐴 ⊆ (V × V)))
2 df-rel 4514 . 2 (Rel 𝐵𝐵 ⊆ (V × V))
3 df-rel 4514 . 2 (Rel 𝐴𝐴 ⊆ (V × V))
41, 2, 33imtr4g 204 1 (𝐴𝐵 → (Rel 𝐵 → Rel 𝐴))
 Colors of variables: wff set class Syntax hints:   → wi 4  Vcvv 2658   ⊆ wss 3039   × cxp 4505  Rel wrel 4512 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097 This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-in 3045  df-ss 3052  df-rel 4514 This theorem is referenced by:  relin1  4625  relin2  4626  reldif  4627  relres  4815  iss  4833  cnvdif  4913  funss  5110  funssres  5133  fliftcnv  5662  fliftfun  5663  reltpos  6113  tpostpos  6127  swoer  6423  erinxp  6469  ltrel  7790  lerel  7792  txdis1cn  12353  xmeter  12511
 Copyright terms: Public domain W3C validator