Theorem relres 5603

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 5291	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		inss2 3995	. . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V)
3	1, 2	eqsstri 3797	. 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V)
4		relxp 5297	. 2 ⊢ Rel (𝐵 × V)
5		relss 5378	. 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵)))
6	3, 4, 5	mp2 9	1 ⊢ Rel (𝐴 ↾ 𝐵)

Syntax hints:  Vcvv 3350   ∩ cin 3733   ⊆ wss 3734   × cxp 5277   ↾ cres 5281  Rel wrel 5284

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-v 3352  df-in 3741  df-ss 3748  df-opab 4874  df-xp 5285  df-rel 5286  df-res 5291

This theorem is referenced by:  elresOLD  5613  iss  5626  dfres2  5632  restidsing  5644  idrefOLD  5694  asymref  5697  poirr2  5705  cnvcnvres  5783  resco  5827  coeq0  5832  ressn  5859  funssres  6113  fnresdisj  6181  fnres  6187  fresaunres2  6260  fcnvres  6266  nfunsn  6417  dffv2  6464  fsnunfv  6650  resfunexgALT  7331  domss2  8330  fidomdm  8454  dmct  9603  relexp0rel  14076  setsres  16187  pospo  17253  metustid  22652  ovoliunlem1  23574  dvres  23980  dvres2  23981  dvlog  24702  efopnlem2  24708  h2hlm  28314  hlimcaui  28570  funresdm1  29885  dfpo2  32111  eqfunresadj  32125  dfrdg2  32165  funpartfun  32515  brres2  34488  elecres  34495  br1cnvssrres  34705  mapfzcons1  37982  diophrw  38024  eldioph2lem1  38025  eldioph2lem2  38026  undmrnresiss  38609  rtrclexi  38627  brfvrcld2  38683  relexpiidm  38695  rp-imass  38763  idhe  38779  limsupresuz  40597  liminfresuz  40678  funressnfv  41844  dfdfat2  41900  setrec2lem2  43134