Theorem relss 5692

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

Syntax hints:   → wi 4  Vcvv 3432   ⊆ wss 3887   × cxp 5587  Rel wrel 5594

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-rel 5596

This theorem is referenced by:  relin1  5722  relin2  5723  reldif  5725  relres  5920  iss  5943  cnvdif  6047  difxp  6067  sofld  6090  funss  6453  funssres  6478  fliftcnv  7182  fliftfun  7183  releldmdifi  7886  frxp  7967  reltpos  8047  swoer  8528  sbthcl  8882  fpwwe2lem8  10394  recmulnq  10720  prcdnq  10749  ltrel  11037  lerel  11039  dfle2  12881  dflt2  12882  isinv  17472  invsym2  17475  invfun  17476  oppcsect2  17491  oppcinv  17492  relfull  17624  relfth  17625  psss  18298  gicer  18892  gsum2d  19573  isunit  19899  txdis1cn  22786  hmpher  22935  tgphaus  23268  qustgplem  23272  tsmsxp  23306  xmeter  23586  ovoliunlem1  24666  taylf  25520  lgsquadlem1  26528  lgsquadlem2  26529  nvrel  28964  phrel  29177  bnrel  29229  hlrel  29252  gonan0  33354  frxp2  33791  frxp3  33797  sscoid  34215  trer  34505  fneer  34542  heicant  35812  iss2  36479  funALTVss  36810  disjss  36842  dvhopellsm  39131  diclspsn  39208  dih1dimatlem  39343