Theorem relss 5729

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

Step	Hyp	Ref	Expression
1		sstr2 3938	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ (V × V) → 𝐴 ⊆ (V × V)))
2		df-rel 5629	. 2 ⊢ (Rel 𝐵 ↔ 𝐵 ⊆ (V × V))
3		df-rel 5629	. 2 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))
4	1, 2, 3	3imtr4g 296	1 ⊢ (𝐴 ⊆ 𝐵 → (Rel 𝐵 → Rel 𝐴))

Syntax hints:   → wi 4  Vcvv 3438   ⊆ wss 3899   × cxp 5620  Rel wrel 5627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810

This theorem depends on definitions:  df-bi 207  df-ss 3916  df-rel 5629

This theorem is referenced by:  relin1  5759  relin2  5760  reldif  5762  relres  5962  iss  5992  cnvdif  6099  difxp  6120  sofld  6143  funss  6509  funssres  6534  fliftcnv  7255  fliftfun  7256  releldmdifi  7987  frxp  8066  frxp2  8084  frxp3  8091  reltpos  8171  swoer  8664  sbthcl  9025  fpwwe2lem8  10547  recmulnq  10873  prcdnq  10902  ltrel  11192  lerel  11194  dfle2  13059  dflt2  13060  isinv  17682  invsym2  17685  invfun  17686  oppcsect2  17701  oppcinv  17702  relfull  17832  relfth  17833  psss  18501  gicer  19204  gsum2d  19899  isunit  20307  txdis1cn  23577  hmpher  23726  tgphaus  24059  qustgplem  24063  tsmsxp  24097  xmeter  24375  ovoliunlem1  25457  taylf  26322  lgsquadlem1  27345  lgsquadlem2  27346  noseqrdgfn  28267  nvrel  30626  phrel  30839  bnrel  30891  hlrel  30914  gsumfs2d  33093  elrgspnsubrunlem2  33279  gonan0  35535  sscoid  36054  trer  36459  fneer  36496  heicant  37795  iss2  38476  funALTVss  38897  disjss  38929  dvhopellsm  41316  diclspsn  41393  dih1dimatlem  41528  gricrel  48107  grlicrel  48194