Theorem relres 5962

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 5634	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		inss2 4188	. . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V)
3	1, 2	eqsstri 3978	. 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V)
4		relxp 5640	. 2 ⊢ Rel (𝐵 × V)
5		relss 5729	. 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵)))
6	3, 4, 5	mp2 9	1 ⊢ Rel (𝐴 ↾ 𝐵)

Syntax hints:  Vcvv 3438   ∩ cin 3898   ⊆ wss 3899   × cxp 5620   ↾ cres 5624  Rel wrel 5627

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-in 3906  df-ss 3916  df-opab 5159  df-xp 5628  df-rel 5629  df-res 5634

This theorem is referenced by:  relresdm1  5990  iss  5992  dfres2  5998  restidsing  6010  asymref  6071  poirr2  6079  cnvcnvres  6161  resco  6206  coeq0  6212  resssxp  6226  ressn  6241  dfpo2  6252  snres0  6254  funssres  6534  fnresdisj  6610  fnres  6617  fresaunres2  6704  fcnvres  6709  nfunsn  6871  dffv2  6927  fsnunfv  7131  eqfunresadj  7304  resfunexgALT  7890  elecres  8681  domss2  9062  fidomdm  9232  ttrclco  9625  cottrcl  9626  dmttrcl  9628  rnttrcl  9629  frmin  9659  frrlem16  9668  frr1  9669  dmct  10432  relexp0rel  14958  setsres  17103  pospo  18264  metustid  24496  ovoliunlem1  25457  dvres  25866  dvres2  25867  dvlog  26614  efopnlem2  26620  noetasuplem2  27700  noetainflem2  27704  h2hlm  31004  hlimcaui  31260  dfrdg2  35936  funpartfun  36086  bj-idreseq  37306  bj-idreseqb  37307  brres2  38405  br1cnvssrres  38697  refrelressn  38716  trrelressn  38779  dfeldisj2  38916  dfeldisj3  38917  dfeldisj4  38918  disjres  38942  antisymrelres  38961  antisymrelressn  38962  mapfzcons1  42901  diophrw  42943  eldioph2lem1  42944  eldioph2lem2  42945  undmrnresiss  43787  brfvrcld2  43875  relexpiidm  43887  limsupresuz  45889  liminfresuz  45970  funressnfv  47231  dfdfat2  47316  resinsn  49059  resinsnALT  49060  tposres0  49064  setrec2lem2  49881