Theorem relss 5408

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

Syntax hints:   → wi 4  Vcvv 3391   ⊆ wss 3769   × cxp 5309  Rel wrel 5316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-in 3776  df-ss 3783  df-rel 5318

This theorem is referenced by:  relin1  5437  relin2  5438  reldif  5440  relres  5629  iss  5652  cnvdif  5750  difxp  5769  sofld  5792  funss  6120  funssres  6144  fliftcnv  6785  fliftfun  6786  frxp  7521  reltpos  7592  tpostpos  7607  swoer  8009  sbthcl  8321  fpwwe2lem9  9745  recmulnq  10071  prcdnq  10100  ltrel  10385  lerel  10387  dfle2  12196  dflt2  12197  isinv  16624  invsym2  16627  invfun  16628  oppcsect2  16643  oppcinv  16644  relfull  16772  relfth  16773  psss  17419  gicer  17920  gsum2d  18572  isunit  18859  opsrtoslem2  19693  txdis1cn  21652  hmpher  21801  tgphaus  22133  qustgplem  22137  tsmsxp  22171  xmeter  22451  ovoliunlem1  23483  taylf  24329  lgsquadlem1  25319  lgsquadlem2  25320  nvrel  27785  phrel  27998  bnrel  28051  hlrel  28074  elrn3  31974  sscoid  32341  trer  32631  fneer  32669  heicant  33757  iss2  34425  dvhopellsm  36898  diclspsn  36975  dih1dimatlem  37110