Theorem relss 5658

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

Syntax hints:   → wi 4  Vcvv 3496   ⊆ wss 3938   × cxp 5555  Rel wrel 5562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-in 3945  df-ss 3954  df-rel 5564

This theorem is referenced by:  relin1  5687  relin2  5688  reldif  5690  relres  5884  iss  5905  cnvdif  6004  difxp  6023  sofld  6046  funss  6376  funssres  6400  fliftcnv  7066  fliftfun  7067  releldmdifi  7746  frxp  7822  reltpos  7899  swoer  8321  sbthcl  8641  fpwwe2lem9  10062  recmulnq  10388  prcdnq  10417  ltrel  10705  lerel  10707  dfle2  12543  dflt2  12544  isinv  17032  invsym2  17035  invfun  17036  oppcsect2  17051  oppcinv  17052  relfull  17180  relfth  17181  psss  17826  gicer  18418  gsum2d  19094  isunit  19409  txdis1cn  22245  hmpher  22394  tgphaus  22727  qustgplem  22731  tsmsxp  22765  xmeter  23045  ovoliunlem1  24105  taylf  24951  lgsquadlem1  25958  lgsquadlem2  25959  nvrel  28381  phrel  28594  bnrel  28646  hlrel  28669  gonan0  32641  sscoid  33376  trer  33666  fneer  33703  heicant  34929  iss2  35603  funALTVss  35934  disjss  35966  dvhopellsm  38255  diclspsn  38332  dih1dimatlem  38467