Theorem relss 5736

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

Syntax hints:   → wi 4  Vcvv 3444   ⊆ wss 3911   × cxp 5629  Rel wrel 5636

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

This theorem depends on definitions:  df-bi 207  df-ss 3928  df-rel 5638

This theorem is referenced by:  relin1  5766  relin2  5767  reldif  5769  relres  5965  iss  5995  cnvdif  6104  difxp  6125  sofld  6148  funss  6519  funssres  6544  fliftcnv  7268  fliftfun  7269  releldmdifi  8003  frxp  8082  frxp2  8100  frxp3  8107  reltpos  8187  swoer  8679  sbthcl  9040  fpwwe2lem8  10567  recmulnq  10893  prcdnq  10922  ltrel  11212  lerel  11214  dfle2  13083  dflt2  13084  isinv  17698  invsym2  17701  invfun  17702  oppcsect2  17717  oppcinv  17718  relfull  17848  relfth  17849  psss  18515  gicer  19185  gsum2d  19878  isunit  20258  txdis1cn  23498  hmpher  23647  tgphaus  23980  qustgplem  23984  tsmsxp  24018  xmeter  24297  ovoliunlem1  25379  taylf  26244  lgsquadlem1  27267  lgsquadlem2  27268  noseqrdgfn  28176  nvrel  30504  phrel  30717  bnrel  30769  hlrel  30792  gsumfs2d  32968  elrgspnsubrunlem2  33172  gonan0  35352  sscoid  35874  trer  36277  fneer  36314  heicant  37622  iss2  38299  funALTVss  38664  disjss  38696  dvhopellsm  41084  diclspsn  41161  dih1dimatlem  41296  gricrel  47892  grlicrel  47971