Theorem relres 5992

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 5666	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		inss2 4213	. . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V)
3	1, 2	eqsstri 4005	. 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V)
4		relxp 5672	. 2 ⊢ Rel (𝐵 × V)
5		relss 5760	. 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵)))
6	3, 4, 5	mp2 9	1 ⊢ Rel (𝐴 ↾ 𝐵)

Syntax hints:  Vcvv 3459   ∩ cin 3925   ⊆ wss 3926   × cxp 5652   ↾ cres 5656  Rel wrel 5659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-in 3933  df-ss 3943  df-opab 5182  df-xp 5660  df-rel 5661  df-res 5666

This theorem is referenced by:  relresdm1  6020  iss  6022  dfres2  6028  restidsing  6040  asymref  6105  poirr2  6113  cnvcnvres  6194  resco  6239  coeq0  6244  resssxp  6259  ressn  6274  dfpo2  6285  snres0  6287  funssres  6580  fnresdisj  6658  fnres  6665  fresaunres2  6750  fcnvres  6755  nfunsn  6918  dffv2  6974  fsnunfv  7179  eqfunresadj  7353  resfunexgALT  7946  domss2  9150  fidomdm  9346  ttrclco  9732  cottrcl  9733  dmttrcl  9735  rnttrcl  9736  frmin  9763  frrlem16  9772  frr1  9773  dmct  10538  relexp0rel  15056  setsres  17197  pospo  18355  metustid  24493  ovoliunlem1  25455  dvres  25864  dvres2  25865  dvlog  26612  efopnlem2  26618  noetasuplem2  27698  noetainflem2  27702  h2hlm  30961  hlimcaui  31217  dfrdg2  35813  funpartfun  35961  bj-idreseq  37180  bj-idreseqb  37181  brres2  38286  elecres  38295  br1cnvssrres  38523  refrelressn  38542  trrelressn  38601  dfeldisj2  38736  dfeldisj3  38737  dfeldisj4  38738  disjres  38762  antisymrelres  38781  antisymrelressn  38782  mapfzcons1  42740  diophrw  42782  eldioph2lem1  42783  eldioph2lem2  42784  undmrnresiss  43628  brfvrcld2  43716  relexpiidm  43728  limsupresuz  45732  liminfresuz  45813  funressnfv  47072  dfdfat2  47157  resinsn  48847  resinsnALT  48848  tposres0  48852  setrec2lem2  49558