Theorem relres 5089

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 ( A |` B )

Proof of Theorem relres

Step	Hyp	Ref	Expression
1		df-res 4803	. . 3 |- ( A |` B ) = ( A i^i ( B X. _V ) )
2		inss2 3621	. . 3 |- ( A i^i ( B X. _V ) ) C_ ( B X. _V )
3	1, 2	eqsstri 3432	. 2 |- ( A |` B ) C_ ( B X. _V )
4		relxp 4899	. 2 |- Rel ( B X. _V )
5		relss 4879	. 2 |- ( ( A |` B ) C_ ( B X. _V ) -> ( Rel ( B X. _V ) -> Rel ( A |` B ) ) )
6	3, 4, 5	mp2 9	1 |- Rel ( A |` B )

Syntax hints:   _Vcvv 3017   i^i cin 3373   C_ wss 3374   X. cxp 4789   |` cres 4793   Rel wrel 4796

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-v 3019  df-in 3381  df-ss 3388  df-opab 4421  df-xp 4797  df-rel 4798  df-res 4803

This theorem is referenced by:  elres  5097  iss  5109  dfres2  5114  restidsing  5118  issref  5170  asymref  5173  poirr2  5181  cnvcnvres  5256  resco  5296  coeq0  5301  ressn  5329  funssres  5579  fnresdisj  5642  fnres  5648  fresaunres2  5710  fcnvres  5715  nfunsn  5851  dffv2  5893  fsnunfv  6058  resiexg  6682  resfunexgALT  6709  domss2  7679  fidomdm  7801  relexp0rel  13039  setsres  15089  pospo  16157  metustid  21506  ovoliunlem1  22392  dvres  22803  dvres2  22804  dvlog  23533  efopnlem2  23539  h2hlm  26570  hlimcaui  26826  dmct  28243  dfpo2  30341  dfrdg2  30388  funpartfun  30654  mapfzcons1  35471  diophrw  35513  eldioph2lem1  35514  eldioph2lem2  35515  undmrnresiss  36123  rtrclexi  36141  brfvrcld2  36197  relexpiidm  36209  rp-imass  36279  idhe  36296  funressnfv  38443  dfdfat2  38446