Theorem relss 5762

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

This proof depends on syntax axioms:   → wi 4  Vcvv 3450   ⊆ wss 3899   × cxp 5653  Rel wrel 5660

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 3916  df-rel 5662

This theorem is used by:  relin1  5793  relin2  5794  reldif  5796  relres  5998  iss  6031  cnvdif  6134  difxp  6156  sofld  6180  funss  6552  funssres  6577  fliftcnv  7312  fliftfun  7313  releldmdifi  8042  frxp  8124  frxp2  8142  frxp3  8149  reltpos  8229  swoer  8728  sbthcl  9097  fpwwe2lem8  10647  recmulnq  10973  prcdnq  11002  ltrel  11295  lerel  11297  dfle2  13198  dflt2  13199  isinv  17849  invsym2  17852  invfun  17853  oppcsect2  17868  oppcinv  17869  relfull  17999  relfth  18000  psss  18668  gicer  19404  gsum2d  20099  isunit  20514  ricrel  20655  txdis1cn  23861  hmpher  24010  tgphaus  24343  qustgplem  24347  tsmsxp  24381  xmeter  24659  ovoliunlem1  25730  taylf  26597  lgsquadlem1  27616  lgsquadlem2  27617  noseqrdgfn  28571  nvrel  31083  phrel  31296  bnrel  31348  hlrel  31371  gsumfs2d  33501  elrgspnsubrunlem2  33688  gonan0  35971  sscoid  36490  trer  36935  fneer  36972  heicant  38404  iss2  39092  funALTVss  39532  disjss  39579  dvhopellsm  41990  diclspsn  42067  dih1dimatlem  42202  gricrel  48835  grlicrel  48922