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

Syntax hints:   → wi 4  Vcvv 3436   ⊆ wss 3903   × cxp 5617  Rel wrel 5624

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 3920  df-rel 5626

This theorem is referenced by:  relin1  5755  relin2  5756  reldif  5758  relres  5956  iss  5986  cnvdif  6092  difxp  6113  sofld  6136  funss  6501  funssres  6526  fliftcnv  7248  fliftfun  7249  releldmdifi  7980  frxp  8059  frxp2  8077  frxp3  8084  reltpos  8164  swoer  8656  sbthcl  9016  fpwwe2lem8  10532  recmulnq  10858  prcdnq  10887  ltrel  11177  lerel  11179  dfle2  13049  dflt2  13050  isinv  17667  invsym2  17670  invfun  17671  oppcsect2  17686  oppcinv  17687  relfull  17817  relfth  17818  psss  18486  gicer  19156  gsum2d  19851  isunit  20258  txdis1cn  23520  hmpher  23669  tgphaus  24002  qustgplem  24006  tsmsxp  24040  xmeter  24319  ovoliunlem1  25401  taylf  26266  lgsquadlem1  27289  lgsquadlem2  27290  noseqrdgfn  28205  nvrel  30546  phrel  30759  bnrel  30811  hlrel  30834  gsumfs2d  33008  elrgspnsubrunlem2  33188  gonan0  35365  sscoid  35887  trer  36290  fneer  36327  heicant  37635  iss2  38312  funALTVss  38677  disjss  38709  dvhopellsm  41096  diclspsn  41173  dih1dimatlem  41308  gricrel  47903  grlicrel  47990