Theorem relres 5998

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 5667	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		inss2 4183	. . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V)
3	1, 2	eqsstri 3977	. 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V)
4		relxp 5673	. 2 ⊢ Rel (𝐵 × V)
5		relss 5762	. 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵)))
6	3, 4, 5	mp2 9	1 ⊢ Rel (𝐴 ↾ 𝐵)

This proof depends on syntax axioms:  Vcvv 3450   ∩ cin 3898   ⊆ wss 3899   × cxp 5653   ↾ cres 5657  Rel wrel 5660

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-in 3906  df-ss 3916  df-opab 5168  df-xp 5661  df-rel 5662  df-res 5667

This theorem is used by:  resindm  6023  relresdm1  6029  iss  6031  dfres2  6037  restidsing  6049  asymref  6110  poirr2  6118  cnvcnvres  6201  resco  6246  coeq0  6252  resssxp  6267  ressn  6283  dfpo2  6294  snres0  6296  funssres  6578  fnresdisj  6653  fnres  6660  fresaunres2  6748  fcnvres  6753  nfunsn  6918  dffv2  6974  fsnunfv  7186  eqfunresadj  7364  resfunexgALT  7946  elecres  8746  domss2  9135  fidomdm  9302  ttrclco  9698  cottrcl  9699  dmttrcl  9701  rnttrcl  9702  frmin  9732  frrlem16  9741  frr1  9742  dmct  10527  dmctOLD  10528  relexp0rel  15111  setsres  17271  pospo  18432  metustid  24781  ovoliunlem1  25731  dvres  26139  dvres2  26140  dvlog  26889  efopnlem2  26895  noetasuplem2  27971  noetainflem2  27975  h2hlm  31462  hlimcaui  31718  dfrdg2  36373  funpartfun  36523  bj-idreseq  37915  bj-idreseqb  37916  brres2  39022  br1cnvssrres  39334  refrelressn  39353  trrelressn  39416  dfeldisj2  39559  dfeldisj3  39560  dfeldisj4  39561  disjres  39593  antisymrelres  39615  antisymrelressn  39616  mapfzcons1  43563  diophrw  43605  eldioph2lem1  43606  eldioph2lem2  43607  undmrnresiss  44445  brfvrcld2  44533  relexpiidm  44545  limsupresuz  46532  liminfresuz  46613  funressnfv  47932  dfdfat2  48017  resinsn  49799  resinsnALT  49800  tposres0  49804  setrec2lem2  50621