Theorem relres 5238

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 4952	. . 3 |- ( A |` B ) = ( A i^i ( B X. _V ) )
2		inss2 3671	. . 3 |- ( A i^i ( B X. _V ) ) C_ ( B X. _V )
3	1, 2	eqsstri 3486	. 2 |- ( A |` B ) C_ ( B X. _V )
4		relxp 5047	. 2 |- Rel ( B X. _V )
5		relss 5027	. 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 3070   i^i cin 3427   C_ wss 3428   X. cxp 4938   |` cres 4942   Rel wrel 4945

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-v 3072  df-in 3435  df-ss 3442  df-opab 4451  df-xp 4946  df-rel 4947  df-res 4952

This theorem is referenced by:  elres  5245  iss  5254  dfres2  5258  restidsing  5262  issref  5311  asymref  5314  poirr2  5322  cnvcnvres  5402  resco  5442  ressn  5473  funssres  5558  fnresdisj  5621  fnres  5627  fresaunres2  5683  fcnvres  5688  nfunsn  5822  dffv2  5865  fsnunfv  6019  resiexg  6616  resfunexgALT  6642  domss2  7572  fidomdm  7696  setsres  14306  pospo  15247  metustidOLD  20252  metustid  20253  ovoliunlem1  21103  dvres  21504  dvres2  21505  dvlog  22214  efopnlem2  22220  h2hlm  24519  hlimcaui  24776  dmct  26150  dfpo2  27701  dfrdg2  27745  funpartfun  28110  mapfzcons1  29193  coeq0  29230  diophrw  29237  eldioph2lem1  29238  eldioph2lem2  29239  funressnfv  30174  dfdfat2  30177