Metamath Proof Explorer

Theorem dfres4

Description: Alternate definition of the restriction of a class. (Contributed by Peter Mazsa, 2-Jan-2019)

Ref Expression
Assertion dfres4 
|- ( R |` A ) = ( R i^i ( A X. ran ( R |` A ) ) )

Proof

Step Hyp Ref Expression
1 dfres2 
 |-  ( R |` A ) = { <. x , y >. | ( x e. A /\ x R y ) }
2 inxprnres 
 |-  ( R i^i ( A X. ran ( R |` A ) ) ) = { <. x , y >. | ( x e. A /\ x R y ) }
3 1 2 eqtr4i 
 |-  ( R |` A ) = ( R i^i ( A X. ran ( R |` A ) ) )