Theorem relss 5206

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

Syntax hints:   → wi 4  Vcvv 3200   ⊆ wss 3574   × cxp 5112  Rel wrel 5119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588  df-rel 5121

This theorem is referenced by:  relin1  5236  relin2  5237  reldif  5238  relres  5426  iss  5447  cnvdif  5539  difxp  5558  sofld  5581  funss  5907  funssres  5930  fliftcnv  6561  fliftfun  6562  frxp  7287  reltpos  7357  tpostpos  7372  swoer  7772  erinxp  7821  sbthcl  8082  fpwwe2lem8  9459  fpwwe2lem9  9460  fpwwe2lem12  9463  recmulnq  9786  prcdnq  9815  ltrel  10100  lerel  10102  dfle2  11980  dflt2  11981  pwsle  16152  isinv  16420  invsym2  16423  invfun  16424  oppcsect2  16439  oppcinv  16440  relfull  16568  relfth  16569  psss  17214  gicer  17718  gicerOLD  17719  gsum2d  18371  isunit  18657  opsrtoslem2  19485  txdis1cn  21438  hmpher  21587  tgphaus  21920  qustgplem  21924  tsmsxp  21958  xmeter  22238  ovoliunlem1  23270  taylf  24115  lgsquadlem1  25105  lgsquadlem2  25106  nvrel  27457  phrel  27670  bnrel  27723  hlrel  27746  elrn3  31652  sscoid  32020  trer  32310  fneer  32348  heicant  33444  iss2  34112  dvhopellsm  36406  diclspsn  36483  dih1dimatlem  36618