Theorem relss 5769

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

Syntax hints:   → wi 4  Vcvv 3463   ⊆ wss 3913   × cxp 5660  Rel wrel 5667

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

This theorem depends on definitions:  df-bi 210  df-ss 3930  df-rel 5669

This theorem is referenced by:  relin1  5800  relin2  5801  reldif  5803  relres  6005  iss  6038  cnvdif  6141  difxp  6162  sofld  6186  funss  6556  funssres  6581  fliftcnv  7310  fliftfun  7311  releldmdifi  8041  frxp  8121  frxp2  8139  frxp3  8146  reltpos  8226  swoer  8725  sbthcl  9086  fpwwe2lem8  10622  recmulnq  10948  prcdnq  10977  ltrel  11270  lerel  11272  dfle2  13171  dflt2  13172  isinv  17816  invsym2  17819  invfun  17820  oppcsect2  17835  oppcinv  17836  relfull  17966  relfth  17967  psss  18635  gicer  19346  gsum2d  20041  isunit  20454  txdis1cn  23760  hmpher  23909  tgphaus  24242  qustgplem  24246  tsmsxp  24280  xmeter  24558  ovoliunlem1  25629  taylf  26489  lgsquadlem1  27509  lgsquadlem2  27510  noseqrdgfn  28464  nvrel  30894  phrel  31107  bnrel  31159  hlrel  31182  gsumfs2d  33321  elrgspnsubrunlem2  33508  gonan0  35782  sscoid  36301  trer  36715  fneer  36752  heicant  38193  iss2  38882  funALTVss  39322  disjss  39369  dvhopellsm  41780  diclspsn  41857  dih1dimatlem  41992  gricrel  48572  grlicrel  48659