Theorem relss 5768

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

Syntax hints:   → wi 4  Vcvv 3455   ⊆ wss 3905   × cxp 5659  Rel wrel 5666

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

This theorem depends on definitions:  df-bi 210  df-ss 3922  df-rel 5668

This theorem is referenced by:  relin1  5799  relin2  5800  reldif  5802  relres  6004  iss  6037  cnvdif  6140  difxp  6161  sofld  6185  funss  6555  funssres  6580  fliftcnv  7309  fliftfun  7310  releldmdifi  8038  frxp  8118  frxp2  8136  frxp3  8143  reltpos  8223  swoer  8722  sbthcl  9083  fpwwe2lem8  10618  recmulnq  10944  prcdnq  10973  ltrel  11266  lerel  11268  dfle2  13167  dflt2  13168  isinv  17812  invsym2  17815  invfun  17816  oppcsect2  17831  oppcinv  17832  relfull  17962  relfth  17963  psss  18631  gicer  19342  gsum2d  20037  isunit  20451  ricrel  20592  txdis1cn  23792  hmpher  23941  tgphaus  24274  qustgplem  24278  tsmsxp  24312  xmeter  24590  ovoliunlem1  25661  taylf  26524  lgsquadlem1  27544  lgsquadlem2  27545  noseqrdgfn  28499  nvrel  30954  phrel  31167  bnrel  31219  hlrel  31242  gsumfs2d  33381  elrgspnsubrunlem2  33568  gonan0  35884  sscoid  36403  trer  36827  fneer  36864  heicant  38306  iss2  38993  funALTVss  39433  disjss  39480  dvhopellsm  41891  diclspsn  41968  dih1dimatlem  42103  gricrel  48684  grlicrel  48771