Theorem relres 6003

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

This proof depends on syntax axioms:  Vcvv 3454   ∩ cin 3903   ⊆ wss 3904   × cxp 5658   ↾ cres 5662  Rel wrel 5665

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-in 3911  df-ss 3921  df-opab 5173  df-xp 5666  df-rel 5667  df-res 5672

This theorem is used by:  resindm  6028  relresdm1  6034  iss  6036  dfres2  6042  restidsing  6054  asymref  6115  poirr2  6123  cnvcnvres  6205  resco  6250  coeq0  6256  resssxp  6271  ressn  6286  dfpo2  6297  snres0  6299  funssres  6580  fnresdisj  6655  fnres  6662  fresaunres2  6750  fcnvres  6755  nfunsn  6920  dffv2  6976  fsnunfv  7185  eqfunresadj  7360  resfunexgALT  7943  elecres  8741  domss2  9122  fidomdm  9289  ttrclco  9685  cottrcl  9686  dmttrcl  9688  rnttrcl  9689  frmin  9719  frrlem16  9728  frr1  9729  dmct  10514  relexp0rel  15081  setsres  17244  pospo  18405  metustid  24722  ovoliunlem1  25672  dvres  26081  dvres2  26082  dvlog  26827  efopnlem2  26833  noetasuplem2  27909  noetainflem2  27913  h2hlm  31343  hlimcaui  31599  dfrdg2  36293  funpartfun  36443  bj-idreseq  37834  bj-idreseqb  37835  brres2  38950  br1cnvssrres  39262  refrelressn  39281  trrelressn  39344  dfeldisj2  39487  dfeldisj3  39488  dfeldisj4  39489  disjres  39521  antisymrelres  39543  antisymrelressn  39544  mapfzcons1  43476  diophrw  43518  eldioph2lem1  43519  eldioph2lem2  43520  undmrnresiss  44358  brfvrcld2  44446  relexpiidm  44458  limsupresuz  46445  liminfresuz  46526  funressnfv  47808  dfdfat2  47893  resinsn  49678  resinsnALT  49679  tposres0  49683  setrec2lem2  50500