Theorem relss 5723

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

Syntax hints:   → wi 4  Vcvv 3441   ⊆ wss 3898   × cxp 5618  Rel wrel 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3443  df-in 3905  df-ss 3915  df-rel 5627

This theorem is referenced by:  relin1  5754  relin2  5755  reldif  5757  relres  5952  iss  5975  cnvdif  6082  difxp  6102  sofld  6125  funss  6503  funssres  6528  fliftcnv  7238  fliftfun  7239  releldmdifi  7954  frxp  8034  reltpos  8117  swoer  8599  sbthcl  8960  fpwwe2lem8  10495  recmulnq  10821  prcdnq  10850  ltrel  11138  lerel  11140  dfle2  12982  dflt2  12983  isinv  17569  invsym2  17572  invfun  17573  oppcsect2  17588  oppcinv  17589  relfull  17721  relfth  17722  psss  18395  gicer  18988  gsum2d  19668  isunit  19994  txdis1cn  22892  hmpher  23041  tgphaus  23374  qustgplem  23378  tsmsxp  23412  xmeter  23692  ovoliunlem1  24772  taylf  25626  lgsquadlem1  26634  lgsquadlem2  26635  nvrel  29252  phrel  29465  bnrel  29517  hlrel  29540  gonan0  33653  frxp2  34073  frxp3  34079  sscoid  34311  trer  34601  fneer  34638  heicant  35925  iss2  36618  funALTVss  36974  disjss  37006  dvhopellsm  39393  diclspsn  39470  dih1dimatlem  39605