Theorem relres 5953

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 5626	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		inss2 4185	. . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V)
3	1, 2	eqsstri 3976	. 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V)
4		relxp 5632	. 2 ⊢ Rel (𝐵 × V)
5		relss 5721	. 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵)))
6	3, 4, 5	mp2 9	1 ⊢ Rel (𝐴 ↾ 𝐵)

Syntax hints:  Vcvv 3436   ∩ cin 3896   ⊆ wss 3897   × cxp 5612   ↾ cres 5616  Rel wrel 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-in 3904  df-ss 3914  df-opab 5152  df-xp 5620  df-rel 5621  df-res 5626

This theorem is referenced by:  relresdm1  5981  iss  5983  dfres2  5989  restidsing  6001  asymref  6062  poirr2  6070  cnvcnvres  6152  resco  6197  coeq0  6203  resssxp  6217  ressn  6232  dfpo2  6243  snres0  6245  funssres  6525  fnresdisj  6601  fnres  6608  fresaunres2  6695  fcnvres  6700  nfunsn  6861  dffv2  6917  fsnunfv  7121  eqfunresadj  7294  resfunexgALT  7880  elecres  8670  domss2  9049  fidomdm  9218  ttrclco  9608  cottrcl  9609  dmttrcl  9611  rnttrcl  9612  frmin  9642  frrlem16  9651  frr1  9652  dmct  10415  relexp0rel  14944  setsres  17089  pospo  18249  metustid  24469  ovoliunlem1  25430  dvres  25839  dvres2  25840  dvlog  26587  efopnlem2  26593  noetasuplem2  27673  noetainflem2  27677  h2hlm  30960  hlimcaui  31216  dfrdg2  35837  funpartfun  35987  bj-idreseq  37206  bj-idreseqb  37207  brres2  38304  br1cnvssrres  38596  refrelressn  38615  trrelressn  38678  dfeldisj2  38815  dfeldisj3  38816  dfeldisj4  38817  disjres  38841  antisymrelres  38860  antisymrelressn  38861  mapfzcons1  42809  diophrw  42851  eldioph2lem1  42852  eldioph2lem2  42853  undmrnresiss  43696  brfvrcld2  43784  relexpiidm  43796  limsupresuz  45800  liminfresuz  45881  funressnfv  47142  dfdfat2  47227  resinsn  48971  resinsnALT  48972  tposres0  48976  setrec2lem2  49794