Theorem relss 5506

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

Syntax hints:   → wi 4  Vcvv 3415   ⊆ wss 3829   × cxp 5405  Rel wrel 5412

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-in 3836  df-ss 3843  df-rel 5414

This theorem is referenced by:  relin1  5535  relin2  5536  reldif  5538  relres  5727  iss  5748  cnvdif  5842  difxp  5861  sofld  5884  funss  6207  funssres  6231  fliftcnv  6887  fliftfun  6888  frxp  7625  reltpos  7700  swoer  8119  sbthcl  8435  fpwwe2lem9  9858  recmulnq  10184  prcdnq  10213  ltrel  10503  lerel  10505  dfle2  12357  dflt2  12358  isinv  16888  invsym2  16891  invfun  16892  oppcsect2  16907  oppcinv  16908  relfull  17036  relfth  17037  psss  17682  gicer  18187  gsum2d  18845  isunit  19130  txdis1cn  21947  hmpher  22096  tgphaus  22428  qustgplem  22432  tsmsxp  22466  xmeter  22746  ovoliunlem1  23806  taylf  24652  lgsquadlem1  25658  lgsquadlem2  25659  nvrel  28156  phrel  28369  bnrel  28422  hlrel  28445  sscoid  32901  trer  33191  fneer  33228  heicant  34374  iss2  35053  funALTVss  35383  disjss  35415  dvhopellsm  37704  diclspsn  37781  dih1dimatlem  37916