Theorem relss 5794

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

Syntax hints:   → wi 4  Vcvv 3478   ⊆ wss 3963   × cxp 5687  Rel wrel 5694

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

This theorem depends on definitions:  df-bi 207  df-ss 3980  df-rel 5696

This theorem is referenced by:  relin1  5825  relin2  5826  reldif  5828  relres  6026  iss  6055  cnvdif  6166  difxp  6186  sofld  6209  funss  6587  funssres  6612  fliftcnv  7331  fliftfun  7332  releldmdifi  8069  frxp  8150  frxp2  8168  frxp3  8175  reltpos  8255  swoer  8775  sbthcl  9134  fpwwe2lem8  10676  recmulnq  11002  prcdnq  11031  ltrel  11321  lerel  11323  dfle2  13186  dflt2  13187  isinv  17808  invsym2  17811  invfun  17812  oppcsect2  17827  oppcinv  17828  relfull  17962  relfth  17963  psss  18638  gicer  19308  gsum2d  20005  isunit  20390  txdis1cn  23659  hmpher  23808  tgphaus  24141  qustgplem  24145  tsmsxp  24179  xmeter  24459  ovoliunlem1  25551  taylf  26417  lgsquadlem1  27439  lgsquadlem2  27440  noseqrdgfn  28327  nvrel  30631  phrel  30844  bnrel  30896  hlrel  30919  gsumfs2d  33041  gonan0  35377  sscoid  35895  trer  36299  fneer  36336  heicant  37642  iss2  38326  funALTVss  38681  disjss  38713  dvhopellsm  41100  diclspsn  41177  dih1dimatlem  41312  gricrel  47826  grlicrel  47902