# Metamath Proof Explorer

## Definition df-res

Description: Define the restriction of a class. Definition 6.6(1) of TakeutiZaring p. 24. For example, the expression  ( exp |RR ) (used in reeff1 ) means "the exponential function e to the x, but the exponent x must be in the reals" ( df-ef defines the exponential function, which normally allows the exponent to be a complex number). Another example is that ( F = { <. 2 , 6 >. , <. 3 , 9 >. }  /\ B = { 1 , 2 } ) -> ( F |B ) = { <. 2 , 6 >. } ( ex-res ). We do not introduce a special syntax for the corestriction of a class: it will be expressed either as the intersection ( A i^i ( _V X. B ) ) or as the converse of the restricted converse (see cnvrescnv ). (Contributed by NM, 2-Aug-1994)

Ref Expression
Assertion df-res ${⊢}{{A}↾}_{{B}}={A}\cap \left({B}×\mathrm{V}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cA ${class}{A}$
1 cB ${class}{B}$
2 0 1 cres ${class}\left({{A}↾}_{{B}}\right)$
3 cvv ${class}\mathrm{V}$
4 1 3 cxp ${class}\left({B}×\mathrm{V}\right)$
5 0 4 cin ${class}\left({A}\cap \left({B}×\mathrm{V}\right)\right)$
6 2 5 wceq ${wff}{{A}↾}_{{B}}={A}\cap \left({B}×\mathrm{V}\right)$