Theorem relss 5731

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

Syntax hints:   → wi 4  Vcvv 3440   ⊆ wss 3901   × cxp 5622  Rel wrel 5629

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

This theorem depends on definitions:  df-bi 207  df-ss 3918  df-rel 5631

This theorem is referenced by:  relin1  5761  relin2  5762  reldif  5764  relres  5964  iss  5994  cnvdif  6101  difxp  6122  sofld  6145  funss  6511  funssres  6536  fliftcnv  7257  fliftfun  7258  releldmdifi  7989  frxp  8068  frxp2  8086  frxp3  8093  reltpos  8173  swoer  8666  sbthcl  9027  fpwwe2lem8  10549  recmulnq  10875  prcdnq  10904  ltrel  11194  lerel  11196  dfle2  13061  dflt2  13062  isinv  17684  invsym2  17687  invfun  17688  oppcsect2  17703  oppcinv  17704  relfull  17834  relfth  17835  psss  18503  gicer  19206  gsum2d  19901  isunit  20309  txdis1cn  23579  hmpher  23728  tgphaus  24061  qustgplem  24065  tsmsxp  24099  xmeter  24377  ovoliunlem1  25459  taylf  26324  lgsquadlem1  27347  lgsquadlem2  27348  noseqrdgfn  28302  nvrel  30677  phrel  30890  bnrel  30942  hlrel  30965  gsumfs2d  33144  elrgspnsubrunlem2  33330  gonan0  35586  sscoid  36105  trer  36510  fneer  36547  heicant  37856  iss2  38537  funALTVss  38958  disjss  38990  dvhopellsm  41377  diclspsn  41454  dih1dimatlem  41589  gricrel  48165  grlicrel  48252