Theorem relss 5770

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

This proof depends on syntax axioms:   → wi 4  Vcvv 3457   ⊆ wss 3906   × cxp 5661  Rel wrel 5668

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 3923  df-rel 5670

This theorem is used by:  relin1  5801  relin2  5802  reldif  5804  relres  6006  iss  6039  cnvdif  6142  difxp  6163  sofld  6187  funss  6559  funssres  6584  fliftcnv  7318  fliftfun  7319  releldmdifi  8048  frxp  8128  frxp2  8146  frxp3  8153  reltpos  8233  swoer  8732  sbthcl  9094  fpwwe2lem8  10638  recmulnq  10964  prcdnq  10993  ltrel  11286  lerel  11288  dfle2  13188  dflt2  13189  isinv  17839  invsym2  17842  invfun  17843  oppcsect2  17858  oppcinv  17859  relfull  17989  relfth  17990  psss  18658  gicer  19391  gsum2d  20086  isunit  20501  ricrel  20642  txdis1cn  23843  hmpher  23992  tgphaus  24325  qustgplem  24329  tsmsxp  24363  xmeter  24641  ovoliunlem1  25712  taylf  26575  lgsquadlem1  27595  lgsquadlem2  27596  noseqrdgfn  28550  nvrel  31025  phrel  31238  bnrel  31290  hlrel  31313  gsumfs2d  33445  elrgspnsubrunlem2  33632  gonan0  35921  sscoid  36440  trer  36884  fneer  36921  heicant  38363  iss2  39051  funALTVss  39491  disjss  39538  dvhopellsm  41949  diclspsn  42026  dih1dimatlem  42161  gricrel  48742  grlicrel  48829