Theorem relss 5782

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

Syntax hints:   → wi 4  Vcvv 3475   ⊆ wss 3949   × cxp 5675  Rel wrel 5682

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-rel 5684

This theorem is referenced by:  relin1  5813  relin2  5814  reldif  5816  relres  6011  iss  6036  cnvdif  6144  difxp  6164  sofld  6187  funss  6568  funssres  6593  fliftcnv  7308  fliftfun  7309  releldmdifi  8031  frxp  8112  frxp2  8130  frxp3  8137  reltpos  8216  swoer  8733  sbthcl  9095  fpwwe2lem8  10633  recmulnq  10959  prcdnq  10988  ltrel  11276  lerel  11278  dfle2  13126  dflt2  13127  isinv  17707  invsym2  17710  invfun  17711  oppcsect2  17726  oppcinv  17727  relfull  17859  relfth  17860  psss  18533  gicer  19150  gsum2d  19840  isunit  20187  txdis1cn  23139  hmpher  23288  tgphaus  23621  qustgplem  23625  tsmsxp  23659  xmeter  23939  ovoliunlem1  25019  taylf  25873  lgsquadlem1  26883  lgsquadlem2  26884  nvrel  29855  phrel  30068  bnrel  30120  hlrel  30143  gonan0  34383  sscoid  34885  trer  35201  fneer  35238  heicant  36523  iss2  37213  funALTVss  37569  disjss  37601  dvhopellsm  39988  diclspsn  40065  dih1dimatlem  40200