Theorem relres 5979

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 5653	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
2		inss2 4204	. . 3 ⊢ (𝐴 ∩ (𝐵 × V)) ⊆ (𝐵 × V)
3	1, 2	eqsstri 3996	. 2 ⊢ (𝐴 ↾ 𝐵) ⊆ (𝐵 × V)
4		relxp 5659	. 2 ⊢ Rel (𝐵 × V)
5		relss 5747	. 2 ⊢ ((𝐴 ↾ 𝐵) ⊆ (𝐵 × V) → (Rel (𝐵 × V) → Rel (𝐴 ↾ 𝐵)))
6	3, 4, 5	mp2 9	1 ⊢ Rel (𝐴 ↾ 𝐵)

Syntax hints:  Vcvv 3450   ∩ cin 3916   ⊆ wss 3917   × cxp 5639   ↾ cres 5643  Rel wrel 5646

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-in 3924  df-ss 3934  df-opab 5173  df-xp 5647  df-rel 5648  df-res 5653

This theorem is referenced by:  relresdm1  6007  iss  6009  dfres2  6015  restidsing  6027  asymref  6092  poirr2  6100  cnvcnvres  6181  resco  6226  coeq0  6231  resssxp  6246  ressn  6261  dfpo2  6272  snres0  6274  funssres  6563  fnresdisj  6641  fnres  6648  fresaunres2  6735  fcnvres  6740  nfunsn  6903  dffv2  6959  fsnunfv  7164  eqfunresadj  7338  resfunexgALT  7929  elecres  8722  domss2  9106  fidomdm  9292  ttrclco  9678  cottrcl  9679  dmttrcl  9681  rnttrcl  9682  frmin  9709  frrlem16  9718  frr1  9719  dmct  10484  relexp0rel  15010  setsres  17155  pospo  18311  metustid  24449  ovoliunlem1  25410  dvres  25819  dvres2  25820  dvlog  26567  efopnlem2  26573  noetasuplem2  27653  noetainflem2  27657  h2hlm  30916  hlimcaui  31172  dfrdg2  35790  funpartfun  35938  bj-idreseq  37157  bj-idreseqb  37158  brres2  38264  br1cnvssrres  38503  refrelressn  38522  trrelressn  38581  dfeldisj2  38717  dfeldisj3  38718  dfeldisj4  38719  disjres  38743  antisymrelres  38762  antisymrelressn  38763  mapfzcons1  42712  diophrw  42754  eldioph2lem1  42755  eldioph2lem2  42756  undmrnresiss  43600  brfvrcld2  43688  relexpiidm  43700  limsupresuz  45708  liminfresuz  45789  funressnfv  47048  dfdfat2  47133  resinsn  48864  resinsnALT  48865  tposres0  48869  setrec2lem2  49687