Theorem relss 5781

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

Syntax hints:   → wi 4  Vcvv 3474   ⊆ wss 3948   × cxp 5674  Rel wrel 5681

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965  df-rel 5683

This theorem is referenced by:  relin1  5812  relin2  5813  reldif  5815  relres  6010  iss  6035  cnvdif  6143  difxp  6163  sofld  6186  funss  6567  funssres  6592  fliftcnv  7310  fliftfun  7311  releldmdifi  8033  frxp  8114  frxp2  8132  frxp3  8139  reltpos  8218  swoer  8735  sbthcl  9097  fpwwe2lem8  10635  recmulnq  10961  prcdnq  10990  ltrel  11280  lerel  11282  dfle2  13130  dflt2  13131  isinv  17711  invsym2  17714  invfun  17715  oppcsect2  17730  oppcinv  17731  relfull  17863  relfth  17864  psss  18537  gicer  19191  gsum2d  19881  isunit  20264  txdis1cn  23359  hmpher  23508  tgphaus  23841  qustgplem  23845  tsmsxp  23879  xmeter  24159  ovoliunlem1  25243  taylf  26097  lgsquadlem1  27107  lgsquadlem2  27108  nvrel  30110  phrel  30323  bnrel  30375  hlrel  30398  gonan0  34669  sscoid  35177  trer  35504  fneer  35541  heicant  36826  iss2  37516  funALTVss  37872  disjss  37904  dvhopellsm  40291  diclspsn  40368  dih1dimatlem  40503