Theorem relres 5914

Description: A restriction is a relation. Exercise 12 of [TakeutiZaring] p. 25. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)

Assertion

Ref	Expression
relres	⊢ Rel (𝐴 ↾ 𝐵)

Proof of Theorem relres

Step	Hyp	Ref	Expression
1		df-res 5597	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		inss2 4165	. . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V)
3	1, 2	eqsstri 3956	. 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V)
4		relxp 5603	. 2 ⊢ Rel (𝐵 × V)
5		relss 5687	. 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵)))
6	3, 4, 5	mp2 9	1 ⊢ Rel (𝐴 ↾ 𝐵)

Syntax hints:  Vcvv 3427   ∩ cin 3887   ⊆ wss 3888   × cxp 5583   ↾ cres 5587  Rel wrel 5590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3071  df-v 3429  df-in 3895  df-ss 3905  df-opab 5138  df-xp 5591  df-rel 5592  df-res 5597

This theorem is referenced by:  iss  5937  dfres2  5943  restidsing  5956  asymref  6015  poirr2  6023  cnvcnvres  6102  resco  6148  coeq0  6153  resssxp  6167  ressn  6182  dfpo2  6193  funssres  6467  fnresdisj  6541  fnres  6548  fresaunres2  6635  fcnvres  6640  nfunsn  6798  dffv2  6850  fsnunfv  7046  resfunexgALT  7769  domss2  8877  fidomdm  9042  dmct  10227  relexp0rel  14692  setsres  16823  pospo  18007  metustid  23654  ovoliunlem1  24609  dvres  25018  dvres2  25019  dvlog  25749  efopnlem2  25755  h2hlm  29283  hlimcaui  29539  funresdm1  30885  snres0  33619  eqfunresadj  33683  dfrdg2  33719  ttrclco  33746  cottrcl  33747  dmttrcl  33749  rnttrcl  33750  noetasuplem2  33906  noetainflem2  33910  funpartfun  34214  bj-idreseq  35302  bj-idreseqb  35303  brres2  36376  elecres  36381  br1cnvssrres  36592  dfeldisj2  36798  dfeldisj3  36799  dfeldisj4  36800  mapfzcons1  40497  diophrw  40539  eldioph2lem1  40540  eldioph2lem2  40541  undmrnresiss  41143  brfvrcld2  41231  relexpiidm  41243  limsupresuz  43176  liminfresuz  43257  funressnfv  44466  dfdfat2  44549  setrec2lem2  46330