Theorem relss 5725

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

Syntax hints:   → wi 4  Vcvv 3431   ⊆ wss 3883   × cxp 5616  Rel wrel 5623

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

This theorem depends on definitions:  df-bi 208  df-ss 3900  df-rel 5625

This theorem is referenced by:  relin1  5755  relin2  5756  reldif  5758  relres  5957  iss  5987  cnvdif  6094  difxp  6115  sofld  6138  funss  6504  funssres  6529  fliftcnv  7255  fliftfun  7256  releldmdifi  7987  frxp  8066  frxp2  8084  frxp3  8091  reltpos  8171  swoer  8665  sbthcl  9027  fpwwe2lem8  10552  recmulnq  10878  prcdnq  10907  ltrel  11198  lerel  11200  dfle2  13089  dflt2  13090  isinv  17718  invsym2  17721  invfun  17722  oppcsect2  17737  oppcinv  17738  relfull  17868  relfth  17869  psss  18537  gicer  19243  gsum2d  19938  isunit  20344  txdis1cn  23618  hmpher  23767  tgphaus  24100  qustgplem  24104  tsmsxp  24138  xmeter  24416  ovoliunlem1  25487  taylf  26344  lgsquadlem1  27361  lgsquadlem2  27362  noseqrdgfn  28316  nvrel  30691  phrel  30904  bnrel  30956  hlrel  30979  gsumfs2d  33142  elrgspnsubrunlem2  33329  gonan0  35620  sscoid  36139  trer  36544  fneer  36581  heicant  38022  iss2  38711  funALTVss  39151  disjss  39198  dvhopellsm  41609  diclspsn  41686  dih1dimatlem  41821  gricrel  48410  grlicrel  48497