Theorem relss 5656

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

Syntax hints:   → wi 4  Vcvv 3494   ⊆ wss 3936   × cxp 5553  Rel wrel 5560

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952  df-rel 5562

This theorem is referenced by:  relin1  5685  relin2  5686  reldif  5688  relres  5882  iss  5903  cnvdif  6002  difxp  6021  sofld  6044  funss  6374  funssres  6398  fliftcnv  7064  fliftfun  7065  releldmdifi  7744  frxp  7820  reltpos  7897  swoer  8319  sbthcl  8639  fpwwe2lem9  10060  recmulnq  10386  prcdnq  10415  ltrel  10703  lerel  10705  dfle2  12541  dflt2  12542  isinv  17030  invsym2  17033  invfun  17034  oppcsect2  17049  oppcinv  17050  relfull  17178  relfth  17179  psss  17824  gicer  18416  gsum2d  19092  isunit  19407  txdis1cn  22243  hmpher  22392  tgphaus  22725  qustgplem  22729  tsmsxp  22763  xmeter  23043  ovoliunlem1  24103  taylf  24949  lgsquadlem1  25956  lgsquadlem2  25957  nvrel  28379  phrel  28592  bnrel  28644  hlrel  28667  gonan0  32639  sscoid  33374  trer  33664  fneer  33701  heicant  34942  iss2  35616  funALTVss  35947  disjss  35979  dvhopellsm  38268  diclspsn  38345  dih1dimatlem  38480