Theorem relss 5739

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

Syntax hints:   → wi 4  Vcvv 3442   ⊆ wss 3903   × cxp 5630  Rel wrel 5637

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

This theorem depends on definitions:  df-bi 207  df-ss 3920  df-rel 5639

This theorem is referenced by:  relin1  5769  relin2  5770  reldif  5772  relres  5972  iss  6002  cnvdif  6109  difxp  6130  sofld  6153  funss  6519  funssres  6544  fliftcnv  7267  fliftfun  7268  releldmdifi  7999  frxp  8078  frxp2  8096  frxp3  8103  reltpos  8183  swoer  8677  sbthcl  9039  fpwwe2lem8  10561  recmulnq  10887  prcdnq  10916  ltrel  11206  lerel  11208  dfle2  13073  dflt2  13074  isinv  17696  invsym2  17699  invfun  17700  oppcsect2  17715  oppcinv  17716  relfull  17846  relfth  17847  psss  18515  gicer  19218  gsum2d  19913  isunit  20321  txdis1cn  23591  hmpher  23740  tgphaus  24073  qustgplem  24077  tsmsxp  24111  xmeter  24389  ovoliunlem1  25471  taylf  26336  lgsquadlem1  27359  lgsquadlem2  27360  noseqrdgfn  28314  nvrel  30690  phrel  30903  bnrel  30955  hlrel  30978  gsumfs2d  33155  elrgspnsubrunlem2  33342  gonan0  35608  sscoid  36127  trer  36532  fneer  36569  heicant  37906  iss2  38595  funALTVss  39035  disjss  39082  dvhopellsm  41493  diclspsn  41570  dih1dimatlem  41705  gricrel  48279  grlicrel  48366