Theorem relres 5043

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 4739	. . 3 |- ( A |` B ) = ( A i^i ( B X. _V ) )
2		inss2 3427	. . 3 |- ( A i^i ( B X. _V ) ) C_ ( B X. _V )
3	1, 2	eqsstri 3258	. 2 |- ( A |` B ) C_ ( B X. _V )
4		relxp 4837	. 2 |- Rel ( B X. _V )
5		relss 4815	. 2 |- ( ( A |` B ) C_ ( B X. _V ) -> ( Rel ( B X. _V ) -> Rel ( A |` B ) ) )
6	3, 4, 5	mp2 16	1 |- Rel ( A |` B )

Syntax hints:   _Vcvv 2801   i^i cin 3198   C_ wss 3199   X. cxp 4725   |` cres 4729   Rel wrel 4732

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-v 2803  df-in 3205  df-ss 3212  df-opab 4152  df-xp 4733  df-rel 4734  df-res 4739

This theorem is referenced by:  elres  5051  resiexg  5060  iss  5061  dfres2  5067  restidsing  5071  issref  5121  asymref  5124  poirr2  5131  cnvcnvres  5202  resco  5243  ressn  5279  funssres  5371  fnresdisj  5444  fnres  5451  fcnvres  5522  nfunsn  5679  fsnunfv  5858  resfunexgALT  6275  setsresg  13143