Theorem relss 5766

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

This proof depends on syntax axioms:   → wi 4  Vcvv 3454   ⊆ wss 3900   × cxp 5656  Rel wrel 5663

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ss 3901  df-rel 5665

This theorem is used by:  relin1  5799  relin2  5800  reldif  5802  relresOLD  6013  iss  6045  cnvdif  6152  difxp  6173  sofld  6197  funss  6586  funssres  6612  fliftcnv  7350  fliftfun  7351  releldmdifi  8091  frxp  8175  frxp2  8198  frxp3  8205  reltpos  8286  swoer  8787  sbthcl  9156  fpwwe2lem8  10762  recmulnq  11088  prcdnq  11117  ltrel  11410  lerel  11412  dfle2  13316  dflt2  13317  isinv  17985  invsym2  17988  invfun  17989  oppcsect2  18004  oppcinv  18005  relfull  18135  relfth  18136  psss  18804  gicer  19542  gsum2d  20237  isunit  20654  ricrel  20795  txdis1cn  24009  hmpher  24158  tgphaus  24491  qustgplem  24495  tsmsxp  24529  xmeter  24807  ovoliunlem1  25878  taylf  26745  lgsquadlem1  27764  lgsquadlem2  27765  noseqrdgfn  28749  nvrel  31261  phrel  31474  bnrel  31526  hlrel  31549  gsumfs2d  33721  elrgspnsubrunlem2  33908  gonan0  36365  sscoid  36890  trer  37319  fneer  37356  heicant  38841  iss2  39542  funALTVss  39982  disjss  40029  dvhopellsm  42440  diclspsn  42517  dih1dimatlem  42652  hfstructfun  46293  gricrel  49290  grlicrel  49377