Theorem relss 5758

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

This proof depends on syntax axioms:   → wi 4  Vcvv 3451   ⊆ wss 3899   × cxp 5649  Rel wrel 5656

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 5658

This theorem is used by:  relin1  5790  relin2  5791  reldif  5793  relres  5996  iss  6027  cnvdif  6134  difxp  6155  sofld  6179  funss  6558  funssres  6584  fliftcnv  7319  fliftfun  7320  releldmdifi  8056  frxp  8138  frxp2  8161  frxp3  8168  reltpos  8248  swoer  8749  sbthcl  9118  fpwwe2lem8  10723  recmulnq  11049  prcdnq  11078  ltrel  11371  lerel  11373  dfle2  13276  dflt2  13277  isinv  17935  invsym2  17938  invfun  17939  oppcsect2  17954  oppcinv  17955  relfull  18085  relfth  18086  psss  18754  gicer  19491  gsum2d  20186  isunit  20603  ricrel  20744  txdis1cn  23954  hmpher  24103  tgphaus  24436  qustgplem  24440  tsmsxp  24474  xmeter  24752  ovoliunlem1  25823  taylf  26688  lgsquadlem1  27707  lgsquadlem2  27708  noseqrdgfn  28692  nvrel  31204  phrel  31417  bnrel  31469  hlrel  31492  gsumfs2d  33622  elrgspnsubrunlem2  33809  gonan0  36157  sscoid  36675  trer  37104  fneer  37141  heicant  38573  iss2  39276  funALTVss  39716  disjss  39763  dvhopellsm  42174  diclspsn  42251  dih1dimatlem  42386  hfstructfun  46025  gricrel  49016  grlicrel  49103