Theorem relres 5121

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 4835	. . 3 |- ( A |` B ) = ( A i^i ( B X. _V ) )
2		inss2 3660	. . 3 |- ( A i^i ( B X. _V ) ) C_ ( B X. _V )
3	1, 2	eqsstri 3472	. 2 |- ( A |` B ) C_ ( B X. _V )
4		relxp 4931	. 2 |- Rel ( B X. _V )
5		relss 4911	. 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 3059   i^i cin 3413   C_ wss 3414   X. cxp 4821   |` cres 4825   Rel wrel 4828

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-v 3061  df-in 3421  df-ss 3428  df-opab 4454  df-xp 4829  df-rel 4830  df-res 4835

This theorem is referenced by:  elres  5129  iss  5141  dfres2  5146  restidsing  5150  issref  5201  asymref  5204  poirr2  5212  cnvcnvres  5287  resco  5327  coeq0  5332  ressn  5360  funssres  5609  fnresdisj  5672  fnres  5678  fresaunres2  5740  fcnvres  5745  nfunsn  5880  dffv2  5922  fsnunfv  6091  resiexg  6720  resfunexgALT  6747  domss2  7714  fidomdm  7836  relexp0rel  13019  setsres  14871  pospo  15927  metustidOLD  21354  metustid  21355  ovoliunlem1  22205  dvres  22607  dvres2  22608  dvlog  23326  efopnlem2  23332  h2hlm  26311  hlimcaui  26568  dmct  27983  dfpo2  29968  dfrdg2  30015  funpartfun  30281  mapfzcons1  35011  diophrw  35053  eldioph2lem1  35054  eldioph2lem2  35055  brfvrcld2  35671  relexpiidm  35683  rp-imass  35751  idhe  35768  funressnfv  37581  dfdfat2  37584