Theorem relres 6000

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.) (Proof shortened by BJ, 16-Oct-2026.)

Assertion

Ref	Expression
relres	⊢ Rel (𝐴 ↾ 𝐵)

Proof of Theorem relres

Step	Hyp	Ref	Expression
1		relinxp 5796	. 2 ⊢ Rel (𝐴 ∩ (𝐵 × V))
2		df-res 5666	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
3	2	releqi 5758	. 2 ⊢ (Rel (𝐴 ↾ 𝐵) ↔ Rel (𝐴 ∩ (𝐵 × V)))
4	1, 3	mpbir 234	1 ⊢ Rel (𝐴 ↾ 𝐵)

This proof depends on syntax axioms:  Vcvv 3453   ∩ cin 4091   × cxp 5652   ↾ cres 5656  Rel wrel 5659

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3416  df-v 3455  df-ss 3900  df-in 4093  df-opab 5170  df-xp 5660  df-rel 5661  df-res 5666

This theorem is used by:  resindm  6024  relresdm1  6030  iss  6032  dfres2  6038  restidsing  6050  asymref  6115  poirr2  6123  cnvcnvres  6212  resco  6257  coeq0  6263  resssxp  6278  ressn  6294  dfpo2  6305  snres0  6307  funssres  6592  fnresdisj  6667  fnres  6674  fresaunres2  6762  fcnvres  6767  nfunsn  6932  dffv2  6988  fsnunfv  7199  eqfunresadj  7377  resfunexgALT  7967  elecres  8777  domss2  9166  fidomdm  9334  ttrclco  9729  cottrcl  9730  dmttrcl  9732  rnttrcl  9733  frmin  9763  frrlem16  9772  frr1  9773  setrec2lem2  9986  dmct  10612  dmctOLD  10613  relexp0rel  15202  setsres  17368  pospo  18529  metustid  24885  ovoliunlem1  25835  dvres  26243  dvres2  26244  dvlog  26991  efopnlem2  26997  noetasuplem2  28103  noetainflem2  28107  h2hlm  31594  hlimcaui  31850  dfrdg2  36684  funpartfun  36834  bj-idreseq  38223  bj-idreseqb  38224  brres2  39345  br1cnvssrres  39657  refrelressn  39676  trrelressn  39739  dfeldisj2  39882  dfeldisj3  39883  dfeldisj4  39884  disjres  39916  antisymrelres  39938  antisymrelressn  39939  mapfzcons1  43868  diophrw  43910  eldioph2lem1  43911  eldioph2lem2  43912  undmrnresiss  44744  brfvrcld2  44832  relexpiidm  44844  limsupresuz  46852  liminfresuz  46933  funressnfv  48252  dfdfat2  48337  resinsn  50124  resinsnALT  50125  tposres0  50129