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  17702  invsym2  17705  invfun  17706  oppcsect2  17721  oppcinv  17722  relfull  17852  relfth  17853  psss  18521  gicer  19191  gsum2d  19886  isunit  20293  txdis1cn  23555  hmpher  23704  tgphaus  24037  qustgplem  24041  tsmsxp  24075  xmeter  24354  ovoliunlem1  25436  taylf  26301  lgsquadlem1  27324  lgsquadlem2  27325  noseqrdgfn  28240  nvrel  30581  phrel  30794  bnrel  30846  hlrel  30869  gsumfs2d  33038  elrgspnsubrunlem2  33215  gonan0  35372  sscoid  35894  trer  36297  fneer  36334  heicant  37642  iss2  38319  funALTVss  38684  disjss  38716  dvhopellsm  41104  diclspsn  41181  dih1dimatlem  41316  gricrel  47912  grlicrel  47991