Theorem relss 5790

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

Syntax hints:   → wi 4  Vcvv 3479   ⊆ wss 3950   × cxp 5682  Rel wrel 5689

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808

This theorem depends on definitions:  df-bi 207  df-ss 3967  df-rel 5691

This theorem is referenced by:  relin1  5821  relin2  5822  reldif  5824  relres  6022  iss  6052  cnvdif  6162  difxp  6183  sofld  6206  funss  6584  funssres  6609  fliftcnv  7332  fliftfun  7333  releldmdifi  8071  frxp  8152  frxp2  8170  frxp3  8177  reltpos  8257  swoer  8777  sbthcl  9136  fpwwe2lem8  10679  recmulnq  11005  prcdnq  11034  ltrel  11324  lerel  11326  dfle2  13190  dflt2  13191  isinv  17805  invsym2  17808  invfun  17809  oppcsect2  17824  oppcinv  17825  relfull  17956  relfth  17957  psss  18626  gicer  19296  gsum2d  19991  isunit  20374  txdis1cn  23644  hmpher  23793  tgphaus  24126  qustgplem  24130  tsmsxp  24164  xmeter  24444  ovoliunlem1  25538  taylf  26403  lgsquadlem1  27425  lgsquadlem2  27426  noseqrdgfn  28313  nvrel  30622  phrel  30835  bnrel  30887  hlrel  30910  gsumfs2d  33059  elrgspnsubrunlem2  33253  gonan0  35398  sscoid  35915  trer  36318  fneer  36355  heicant  37663  iss2  38346  funALTVss  38701  disjss  38733  dvhopellsm  41120  diclspsn  41197  dih1dimatlem  41332  gricrel  47893  grlicrel  47971