Theorem relss 5805

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

Syntax hints:   → wi 4  Vcvv 3488   ⊆ wss 3976   × cxp 5698  Rel wrel 5705

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

This theorem depends on definitions:  df-bi 207  df-ss 3993  df-rel 5707

This theorem is referenced by:  relin1  5836  relin2  5837  reldif  5839  relres  6035  iss  6064  cnvdif  6175  difxp  6195  sofld  6218  funss  6597  funssres  6622  fliftcnv  7347  fliftfun  7348  releldmdifi  8086  frxp  8167  frxp2  8185  frxp3  8192  reltpos  8272  swoer  8794  sbthcl  9161  fpwwe2lem8  10707  recmulnq  11033  prcdnq  11062  ltrel  11352  lerel  11354  dfle2  13209  dflt2  13210  isinv  17821  invsym2  17824  invfun  17825  oppcsect2  17840  oppcinv  17841  relfull  17975  relfth  17976  psss  18650  gicer  19317  gsum2d  20014  isunit  20399  txdis1cn  23664  hmpher  23813  tgphaus  24146  qustgplem  24150  tsmsxp  24184  xmeter  24464  ovoliunlem1  25556  taylf  26420  lgsquadlem1  27442  lgsquadlem2  27443  noseqrdgfn  28330  nvrel  30634  phrel  30847  bnrel  30899  hlrel  30922  gonan0  35360  sscoid  35877  trer  36282  fneer  36319  heicant  37615  iss2  38300  funALTVss  38655  disjss  38687  dvhopellsm  41074  diclspsn  41151  dih1dimatlem  41286  gricrel  47772  grlicrel  47823