Metamath Proof Explorer

Theorem inxprnres

Description: Restriction of a class as a class of ordered pairs. (Contributed by Peter Mazsa, 2-Jan-2019)

Ref Expression
Assertion inxprnres 
|- ( R i^i ( A X. ran ( R |` A ) ) ) = { <. x , y >. | ( x e. A /\ x R y ) }

Proof

Step Hyp Ref Expression
1 relinxp 
 |-  Rel ( R i^i ( A X. ran ( R |` A ) ) )
2 relopabv 
 |-  Rel { <. x , y >. | ( x e. A /\ x R y ) }
3 eleq1w 
 |-  ( x = z -> ( x e. A <-> z e. A ) )
4 breq1 
 |-  ( x = z -> ( x R y <-> z R y ) )
5 3 4 anbi12d 
 |-  ( x = z -> ( ( x e. A /\ x R y ) <-> ( z e. A /\ z R y ) ) )
6 breq2 
 |-  ( y = w -> ( z R y <-> z R w ) )
7 6 anbi2d 
 |-  ( y = w -> ( ( z e. A /\ z R y ) <-> ( z e. A /\ z R w ) ) )
8 5 7 opelopabg 
 |-  ( ( z e. _V /\ w e. _V ) -> ( <. z , w >. e. { <. x , y >. | ( x e. A /\ x R y ) } <-> ( z e. A /\ z R w ) ) )
9 8 el2v 
 |-  ( <. z , w >. e. { <. x , y >. | ( x e. A /\ x R y ) } <-> ( z e. A /\ z R w ) )
10 brinxprnres 
 |-  ( w e. _V -> ( z ( R i^i ( A X. ran ( R |` A ) ) ) w <-> ( z e. A /\ z R w ) ) )
11 10 elv 
 |-  ( z ( R i^i ( A X. ran ( R |` A ) ) ) w <-> ( z e. A /\ z R w ) )
12 df-br 
 |-  ( z ( R i^i ( A X. ran ( R |` A ) ) ) w <-> <. z , w >. e. ( R i^i ( A X. ran ( R |` A ) ) ) )
13 9 11 12 3bitr2ri 
 |-  ( <. z , w >. e. ( R i^i ( A X. ran ( R |` A ) ) ) <-> <. z , w >. e. { <. x , y >. | ( x e. A /\ x R y ) } )
14 1 2 13 eqrelriiv 
 |-  ( R i^i ( A X. ran ( R |` A ) ) ) = { <. x , y >. | ( x e. A /\ x R y ) }