Theorem relres 5957

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 5630	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		inss2 4166	. . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V)
3	1, 2	eqsstri 3961	. 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V)
4		relxp 5636	. 2 ⊢ Rel (𝐵 × V)
5		relss 5725	. 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵)))
6	3, 4, 5	mp2 9	1 ⊢ Rel (𝐴 ↾ 𝐵)

Syntax hints:  Vcvv 3431   ∩ cin 3882   ⊆ wss 3883   × cxp 5616   ↾ cres 5620  Rel wrel 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-in 3890  df-ss 3900  df-opab 5135  df-xp 5624  df-rel 5625  df-res 5630

This theorem is referenced by:  relresdm1  5985  iss  5987  dfres2  5993  restidsing  6005  asymref  6066  poirr2  6074  cnvcnvres  6156  resco  6201  coeq0  6207  resssxp  6221  ressn  6236  dfpo2  6247  snres0  6249  funssres  6529  fnresdisj  6605  fnres  6612  fresaunres2  6699  fcnvres  6704  nfunsn  6866  dffv2  6922  fsnunfv  7131  eqfunresadj  7304  resfunexgALT  7890  elecres  8682  domss2  9064  fidomdm  9234  ttrclco  9630  cottrcl  9631  dmttrcl  9633  rnttrcl  9634  frmin  9664  frrlem16  9673  frr1  9674  dmct  10437  relexp0rel  14990  setsres  17139  pospo  18300  metustid  24537  ovoliunlem1  25487  dvres  25896  dvres2  25897  dvlog  26633  efopnlem2  26639  noetasuplem2  27716  noetainflem2  27720  h2hlm  31069  hlimcaui  31325  dfrdg2  36021  funpartfun  36171  bj-idreseq  37522  bj-idreseqb  37523  brres2  38640  br1cnvssrres  38952  refrelressn  38971  trrelressn  39034  dfeldisj2  39177  dfeldisj3  39178  dfeldisj4  39179  disjres  39211  antisymrelres  39233  antisymrelressn  39234  mapfzcons1  43166  diophrw  43208  eldioph2lem1  43209  eldioph2lem2  43210  undmrnresiss  44048  brfvrcld2  44136  relexpiidm  44148  limsupresuz  46146  liminfresuz  46227  funressnfv  47506  dfdfat2  47591  resinsn  49362  resinsnALT  49363  tposres0  49367  setrec2lem2  50184