Theorem relss 5769

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

Syntax hints:   → wi 4  Vcvv 3463   ⊆ wss 3913   × cxp 5660  Rel wrel 5667

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

This theorem depends on definitions:  df-bi 210  df-ss 3930  df-rel 5669

This theorem is referenced by:  relin1  5800  relin2  5801  reldif  5803  relres  6005  iss  6038  cnvdif  6141  difxp  6162  sofld  6186  funss  6556  funssres  6581  fliftcnv  7310  fliftfun  7311  releldmdifi  8042  frxp  8122  frxp2  8140  frxp3  8147  reltpos  8227  swoer  8726  sbthcl  9087  fpwwe2lem8  10623  recmulnq  10949  prcdnq  10978  ltrel  11271  lerel  11273  dfle2  13172  dflt2  13173  isinv  17817  invsym2  17820  invfun  17821  oppcsect2  17836  oppcinv  17837  relfull  17967  relfth  17968  psss  18636  gicer  19347  gsum2d  20042  isunit  20455  txdis1cn  23761  hmpher  23910  tgphaus  24243  qustgplem  24247  tsmsxp  24281  xmeter  24559  ovoliunlem1  25630  taylf  26490  lgsquadlem1  27510  lgsquadlem2  27511  noseqrdgfn  28465  nvrel  30895  phrel  31108  bnrel  31160  hlrel  31183  gsumfs2d  33322  elrgspnsubrunlem2  33509  gonan0  35817  sscoid  36336  trer  36750  fneer  36787  heicant  38228  iss2  38917  funALTVss  39357  disjss  39404  dvhopellsm  41815  diclspsn  41892  dih1dimatlem  42027  gricrel  48607  grlicrel  48694