Theorem relss 5765

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

Syntax hints:   → wi 4  Vcvv 3464   ⊆ wss 3931   × cxp 5657  Rel wrel 5664

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 3948  df-rel 5666

This theorem is referenced by:  relin1  5796  relin2  5797  reldif  5799  relres  5997  iss  6027  cnvdif  6137  difxp  6158  sofld  6181  funss  6560  funssres  6585  fliftcnv  7309  fliftfun  7310  releldmdifi  8049  frxp  8130  frxp2  8148  frxp3  8155  reltpos  8235  swoer  8755  sbthcl  9114  fpwwe2lem8  10657  recmulnq  10983  prcdnq  11012  ltrel  11302  lerel  11304  dfle2  13168  dflt2  13169  isinv  17778  invsym2  17781  invfun  17782  oppcsect2  17797  oppcinv  17798  relfull  17928  relfth  17929  psss  18595  gicer  19265  gsum2d  19958  isunit  20338  txdis1cn  23578  hmpher  23727  tgphaus  24060  qustgplem  24064  tsmsxp  24098  xmeter  24377  ovoliunlem1  25460  taylf  26325  lgsquadlem1  27348  lgsquadlem2  27349  noseqrdgfn  28257  nvrel  30588  phrel  30801  bnrel  30853  hlrel  30876  gsumfs2d  33054  elrgspnsubrunlem2  33248  gonan0  35419  sscoid  35936  trer  36339  fneer  36376  heicant  37684  iss2  38367  funALTVss  38722  disjss  38754  dvhopellsm  41141  diclspsn  41218  dih1dimatlem  41353  gricrel  47912  grlicrel  47991