Theorem relss 5721

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

Syntax hints:   → wi 4  Vcvv 3436   ⊆ wss 3897   × cxp 5612  Rel wrel 5619

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

This theorem depends on definitions:  df-bi 207  df-ss 3914  df-rel 5621

This theorem is referenced by:  relin1  5751  relin2  5752  reldif  5754  relres  5953  iss  5983  cnvdif  6090  difxp  6111  sofld  6134  funss  6500  funssres  6525  fliftcnv  7245  fliftfun  7246  releldmdifi  7977  frxp  8056  frxp2  8074  frxp3  8081  reltpos  8161  swoer  8653  sbthcl  9012  fpwwe2lem8  10529  recmulnq  10855  prcdnq  10884  ltrel  11174  lerel  11176  dfle2  13046  dflt2  13047  isinv  17667  invsym2  17670  invfun  17671  oppcsect2  17686  oppcinv  17687  relfull  17817  relfth  17818  psss  18486  gicer  19189  gsum2d  19884  isunit  20291  txdis1cn  23550  hmpher  23699  tgphaus  24032  qustgplem  24036  tsmsxp  24070  xmeter  24348  ovoliunlem1  25430  taylf  26295  lgsquadlem1  27318  lgsquadlem2  27319  noseqrdgfn  28236  nvrel  30582  phrel  30795  bnrel  30847  hlrel  30870  gsumfs2d  33035  elrgspnsubrunlem2  33215  gonan0  35436  sscoid  35955  trer  36358  fneer  36395  heicant  37703  iss2  38380  funALTVss  38745  disjss  38777  dvhopellsm  41164  diclspsn  41241  dih1dimatlem  41376  gricrel  47958  grlicrel  48045