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 relopab 
 |-  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 ) }