Theorem relss 5754

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 3943	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ (V × V) → 𝐴 ⊆ (V × V)))
2		df-rel 5654	. 2 ⊢ (Rel 𝐵 ↔ 𝐵 ⊆ (V × V))
3		df-rel 5654	. 2 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))
4	1, 2, 3	3imtr4g 298	1 ⊢ (𝐴 ⊆ 𝐵 → (Rel 𝐵 → Rel 𝐴))

Syntax hints:   → wi 4  Vcvv 3454   ⊆ wss 3904   × cxp 5645  Rel wrel 5652

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

This theorem depends on definitions:  df-bi 209  df-ss 3921  df-rel 5654

This theorem is referenced by:  relin1  5785  relin2  5786  reldif  5788  relres  5991  iss  6024  cnvdif  6127  difxp  6149  sofld  6173  funss  6540  funssres  6565  fliftcnv  7295  fliftfun  7296  releldmdifi  8026  frxp  8106  frxp2  8124  frxp3  8131  reltpos  8211  swoer  8710  sbthcl  9071  fpwwe2lem8  10596  recmulnq  10922  prcdnq  10951  ltrel  11244  lerel  11246  dfle2  13149  dflt2  13150  isinv  17793  invsym2  17796  invfun  17797  oppcsect2  17812  oppcinv  17813  relfull  17943  relfth  17944  psss  18612  gicer  19317  gsum2d  20012  isunit  20422  txdis1cn  23695  hmpher  23844  tgphaus  24177  qustgplem  24181  tsmsxp  24215  xmeter  24493  ovoliunlem1  25564  taylf  26424  lgsquadlem1  27444  lgsquadlem2  27445  noseqrdgfn  28399  nvrel  30805  phrel  31018  bnrel  31070  hlrel  31093  gsumfs2d  33241  elrgspnsubrunlem2  33429  gonan0  35742  sscoid  36261  trer  36676  fneer  36713  heicant  38154  iss2  38843  funALTVss  39283  disjss  39330  dvhopellsm  41741  diclspsn  41818  dih1dimatlem  41953  gricrel  48541  grlicrel  48628