Theorem relres 5294

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 5006	. . 3 |- ( A |` B ) = ( A i^i ( B X. _V ) )
2		inss2 3714	. . 3 |- ( A i^i ( B X. _V ) ) C_ ( B X. _V )
3	1, 2	eqsstri 3529	. 2 |- ( A |` B ) C_ ( B X. _V )
4		relxp 5103	. 2 |- Rel ( B X. _V )
5		relss 5083	. 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 3108   i^i cin 3470   C_ wss 3471   X. cxp 4992   |` cres 4996   Rel wrel 4999

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-v 3110  df-in 3478  df-ss 3485  df-opab 4501  df-xp 5000  df-rel 5001  df-res 5006

This theorem is referenced by:  elres  5302  iss  5314  dfres2  5319  restidsing  5323  issref  5373  asymref  5376  poirr2  5384  cnvcnvres  5464  resco  5504  coeq0  5509  ressn  5536  funssres  5621  fnresdisj  5684  fnres  5690  fresaunres2  5750  fcnvres  5755  nfunsn  5890  dffv2  5933  fsnunfv  6094  resiexg  6712  resfunexgALT  6739  domss2  7668  fidomdm  7793  setsres  14509  pospo  15451  metustidOLD  20792  metustid  20793  ovoliunlem1  21643  dvres  22045  dvres2  22046  dvlog  22755  efopnlem2  22761  h2hlm  25561  hlimcaui  25818  dmct  27197  dfpo2  28749  dfrdg2  28793  funpartfun  29158  mapfzcons1  30242  diophrw  30285  eldioph2lem1  30286  eldioph2lem2  30287  funressnfv  31637  dfdfat2  31640  rp-imass  36673