Theorem relss 5787

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

Syntax hints:   → wi 4  Vcvv 3462   ⊆ wss 3947   × cxp 5680  Rel wrel 5687

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

This theorem depends on definitions:  df-bi 206  df-ss 3964  df-rel 5689

This theorem is referenced by:  relin1  5818  relin2  5819  reldif  5821  relres  6015  iss  6044  cnvdif  6155  difxp  6175  sofld  6198  funss  6578  funssres  6603  fliftcnv  7323  fliftfun  7324  releldmdifi  8059  frxp  8140  frxp2  8158  frxp3  8165  reltpos  8246  swoer  8765  sbthcl  9133  fpwwe2lem8  10681  recmulnq  11007  prcdnq  11036  ltrel  11326  lerel  11328  dfle2  13180  dflt2  13181  isinv  17776  invsym2  17779  invfun  17780  oppcsect2  17795  oppcinv  17796  relfull  17930  relfth  17931  psss  18605  gicer  19271  gsum2d  19970  isunit  20355  txdis1cn  23630  hmpher  23779  tgphaus  24112  qustgplem  24116  tsmsxp  24150  xmeter  24430  ovoliunlem1  25522  taylf  26388  lgsquadlem1  27409  lgsquadlem2  27410  noseqrdgfn  28280  nvrel  30535  phrel  30748  bnrel  30800  hlrel  30823  gonan0  35220  sscoid  35737  trer  36028  fneer  36065  heicant  37356  iss2  38042  funALTVss  38397  disjss  38429  dvhopellsm  40816  diclspsn  40893  dih1dimatlem  41028  gricrel  47467  grlicrel  47496