Theorem relres 5426

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 5126	. . 3 |- ( A |` B ) = ( A i^i ( B X. _V ) )
2		inss2 3834	. . 3 |- ( A i^i ( B X. _V ) ) C_ ( B X. _V )
3	1, 2	eqsstri 3635	. 2 |- ( A |` B ) C_ ( B X. _V )
4		relxp 5227	. 2 |- Rel ( B X. _V )
5		relss 5206	. 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 3200   i^i cin 3573   C_ wss 3574   X. cxp 5112   |` cres 5116   Rel wrel 5119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588  df-opab 4713  df-xp 5120  df-rel 5121  df-res 5126

This theorem is referenced by:  elres  5435  iss  5447  dfres2  5453  restidsing  5458  restidsingOLD  5459  issref  5509  asymref  5512  poirr2  5520  cnvcnvres  5598  resco  5639  coeq0  5644  ressn  5671  funssres  5930  fnresdisj  6001  fnres  6007  fresaunres2  6076  fcnvres  6082  nfunsn  6225  dffv2  6271  fsnunfv  6453  resiexg  7102  resfunexgALT  7129  domss2  8119  fidomdm  8243  dmct  9346  relexp0rel  13777  setsres  15901  pospo  16973  metustid  22359  ovoliunlem1  23270  dvres  23675  dvres2  23676  dvlog  24397  efopnlem2  24403  h2hlm  27837  hlimcaui  28093  funresdm1  29416  dfpo2  31645  eqfunresadj  31659  dfrdg2  31701  funpartfun  32050  brres2  34035  elecres  34042  mapfzcons1  37280  diophrw  37322  eldioph2lem1  37323  eldioph2lem2  37324  undmrnresiss  37910  rtrclexi  37928  brfvrcld2  37984  relexpiidm  37996  rp-imass  38065  idhe  38081  limsupresuz  39935  liminfresuz  40016  funressnfv  41208  dfdfat2  41211  setrec2lem2  42441