Theorem relres 5150

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 4864	. . 3 |- ( A |` B ) = ( A i^i ( B X. _V ) )
2		inss2 3664	. . 3 |- ( A i^i ( B X. _V ) ) C_ ( B X. _V )
3	1, 2	eqsstri 3473	. 2 |- ( A |` B ) C_ ( B X. _V )
4		relxp 4960	. 2 |- Rel ( B X. _V )
5		relss 4940	. 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 3056   i^i cin 3414   C_ wss 3415   X. cxp 4850   |` cres 4854   Rel wrel 4857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-v 3058  df-in 3422  df-ss 3429  df-opab 4475  df-xp 4858  df-rel 4859  df-res 4864

This theorem is referenced by:  elres  5158  iss  5170  dfres2  5175  restidsing  5179  issref  5231  asymref  5234  poirr2  5242  cnvcnvres  5317  resco  5357  coeq0  5362  ressn  5390  funssres  5640  fnresdisj  5707  fnres  5713  fresaunres2  5777  fcnvres  5782  nfunsn  5918  dffv2  5960  fsnunfv  6127  resiexg  6755  resfunexgALT  6782  domss2  7756  fidomdm  7878  relexp0rel  13148  setsres  15199  pospo  16267  metustid  21617  ovoliunlem1  22503  dvres  22914  dvres2  22915  dvlog  23644  efopnlem2  23650  h2hlm  26681  hlimcaui  26937  dmct  28346  dfpo2  30443  dfrdg2  30490  funpartfun  30758  mapfzcons1  35603  diophrw  35645  eldioph2lem1  35646  eldioph2lem2  35647  undmrnresiss  36254  rtrclexi  36272  brfvrcld2  36328  relexpiidm  36340  rp-imass  36410  idhe  36427  funressnfv  38666  dfdfat2  38670