Theorem relss 5732

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

Syntax hints:   → wi 4  Vcvv 3430   ⊆ wss 3890   × cxp 5623  Rel wrel 5630

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

This theorem depends on definitions:  df-bi 207  df-ss 3907  df-rel 5632

This theorem is referenced by:  relin1  5762  relin2  5763  reldif  5765  relres  5965  iss  5995  cnvdif  6102  difxp  6123  sofld  6146  funss  6512  funssres  6537  fliftcnv  7260  fliftfun  7261  releldmdifi  7992  frxp  8070  frxp2  8088  frxp3  8095  reltpos  8175  swoer  8669  sbthcl  9031  fpwwe2lem8  10555  recmulnq  10881  prcdnq  10910  ltrel  11201  lerel  11203  dfle2  13092  dflt2  13093  isinv  17721  invsym2  17724  invfun  17725  oppcsect2  17740  oppcinv  17741  relfull  17871  relfth  17872  psss  18540  gicer  19246  gsum2d  19941  isunit  20347  txdis1cn  23613  hmpher  23762  tgphaus  24095  qustgplem  24099  tsmsxp  24133  xmeter  24411  ovoliunlem1  25482  taylf  26340  lgsquadlem1  27360  lgsquadlem2  27361  noseqrdgfn  28315  nvrel  30691  phrel  30904  bnrel  30956  hlrel  30979  gsumfs2d  33140  elrgspnsubrunlem2  33327  gonan0  35593  sscoid  36112  trer  36517  fneer  36554  heicant  37993  iss2  38682  funALTVss  39122  disjss  39169  dvhopellsm  41580  diclspsn  41657  dih1dimatlem  41792  gricrel  48410  grlicrel  48497