Metamath Proof Explorer

Theorem bj-dfres2

Description: Alternate definition of the restriction of a class to another, as an ordered pair class abstraction: the restriction of a class to another is the class of ordered pairs whose first component is in the restricting class and whose components are related by the restricted class. (Contributed by Mario Carneiro, 5-Nov-2013) Do not depend on df-rel . (Revised by BJ, 16-Oct-2026)

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

Proof

Step Hyp Ref Expression
1 df-rex 
 |-  ( E. x e. A E. y ( z = <. x , y >. /\ x R y ) <-> E. x ( x e. A /\ E. y ( z = <. x , y >. /\ x R y ) ) )
2 an12 
 |-  ( ( z = <. x , y >. /\ ( x e. A /\ x R y ) ) <-> ( x e. A /\ ( z = <. x , y >. /\ x R y ) ) )
3 2 exbii 
 |-  ( E. y ( z = <. x , y >. /\ ( x e. A /\ x R y ) ) <-> E. y ( x e. A /\ ( z = <. x , y >. /\ x R y ) ) )
4 19.42v 
 |-  ( E. y ( x e. A /\ ( z = <. x , y >. /\ x R y ) ) <-> ( x e. A /\ E. y ( z = <. x , y >. /\ x R y ) ) )
5 3 4 bitr2i 
 |-  ( ( x e. A /\ E. y ( z = <. x , y >. /\ x R y ) ) <-> E. y ( z = <. x , y >. /\ ( x e. A /\ x R y ) ) )
6 5 exbii 
 |-  ( E. x ( x e. A /\ E. y ( z = <. x , y >. /\ x R y ) ) <-> E. x E. y ( z = <. x , y >. /\ ( x e. A /\ x R y ) ) )
7 1 6 bitri 
 |-  ( E. x e. A E. y ( z = <. x , y >. /\ x R y ) <-> E. x E. y ( z = <. x , y >. /\ ( x e. A /\ x R y ) ) )
8 bj-elres 
 |-  ( z e. ( R |` A ) <-> E. x e. A E. y ( z = <. x , y >. /\ x R y ) )
9 elopab 
 |-  ( z e. { <. x , y >. | ( x e. A /\ x R y ) } <-> E. x E. y ( z = <. x , y >. /\ ( x e. A /\ x R y ) ) )
10 7 8 9 3bitr4i 
 |-  ( z e. ( R |` A ) <-> z e. { <. x , y >. | ( x e. A /\ x R y ) } )
11 10 eqriv 
 |-  ( R |` A ) = { <. x , y >. | ( x e. A /\ x R y ) }