Theorem relres 5675

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 5367	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		inss2 4054	. . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V)
3	1, 2	eqsstri 3854	. 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V)
4		relxp 5373	. 2 ⊢ Rel (𝐵 × V)
5		relss 5454	. 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵)))
6	3, 4, 5	mp2 9	1 ⊢ Rel (𝐴 ↾ 𝐵)

Syntax hints:  Vcvv 3398   ∩ cin 3791   ⊆ wss 3792   × cxp 5353   ↾ cres 5357  Rel wrel 5360

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-v 3400  df-in 3799  df-ss 3806  df-opab 4949  df-xp 5361  df-rel 5362  df-res 5367

This theorem is referenced by:  elresOLD  5685  iss  5697  dfres2  5703  restidsing  5714  idrefOLD  5764  asymref  5767  poirr2  5775  cnvcnvres  5852  resco  5893  coeq0  5898  ressn  5925  funssres  6178  fnresdisj  6247  fnres  6253  fresaunres2  6326  fcnvres  6332  nfunsn  6484  dffv2  6531  fsnunfv  6724  resfunexgALT  7408  domss2  8407  fidomdm  8531  dmct  9681  relexp0rel  14184  setsres  16297  pospo  17359  metustid  22767  ovoliunlem1  23706  dvres  24112  dvres2  24113  dvlog  24834  efopnlem2  24840  h2hlm  28409  hlimcaui  28665  funresdm1  29979  dfpo2  32239  eqfunresadj  32252  dfrdg2  32289  funpartfun  32639  brres2  34669  elecres  34676  br1cnvssrres  34885  mapfzcons1  38244  diophrw  38286  eldioph2lem1  38287  eldioph2lem2  38288  undmrnresiss  38871  rtrclexi  38889  brfvrcld2  38945  relexpiidm  38957  rp-imass  39025  idhe  39041  limsupresuz  40847  liminfresuz  40928  funressnfv  42111  dfdfat2  42173  setrec2lem2  43550