Metamath Proof Explorer


Theorem dfres2

Description: Alternate definition of the restriction operation. (Contributed by Mario Carneiro, 5-Nov-2013)

Ref Expression
Assertion dfres2
|- ( R |` A ) = { <. x , y >. | ( x e. A /\ x R y ) }

Proof

Step Hyp Ref Expression
1 relres
 |-  Rel ( R |` A )
2 relopabv
 |-  Rel { <. x , y >. | ( x e. A /\ x R y ) }
3 vex
 |-  z e. _V
4 vex
 |-  w e. _V
5 eleq1w
 |-  ( x = z -> ( x e. A <-> z e. A ) )
6 breq1
 |-  ( x = z -> ( x R y <-> z R y ) )
7 5 6 anbi12d
 |-  ( x = z -> ( ( x e. A /\ x R y ) <-> ( z e. A /\ z R y ) ) )
8 breq2
 |-  ( y = w -> ( z R y <-> z R w ) )
9 8 anbi2d
 |-  ( y = w -> ( ( z e. A /\ z R y ) <-> ( z e. A /\ z R w ) ) )
10 3 4 7 9 opelopab
 |-  ( <. z , w >. e. { <. x , y >. | ( x e. A /\ x R y ) } <-> ( z e. A /\ z R w ) )
11 4 brresi
 |-  ( z ( R |` A ) w <-> ( z e. A /\ z R w ) )
12 df-br
 |-  ( z ( R |` A ) w <-> <. z , w >. e. ( R |` A ) )
13 10 11 12 3bitr2ri
 |-  ( <. z , w >. e. ( R |` A ) <-> <. z , w >. e. { <. x , y >. | ( x e. A /\ x R y ) } )
14 1 2 13 eqrelriiv
 |-  ( R |` A ) = { <. x , y >. | ( x e. A /\ x R y ) }