Metamath Proof Explorer

Theorem resopab

Description: Restriction of a class abstraction of ordered pairs. (Contributed by NM, 5-Nov-2002)

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

Proof

Step Hyp Ref Expression
1 df-res 
 |-  ( { <. x , y >. | ph } |` A ) = ( { <. x , y >. | ph } i^i ( A X. _V ) )
2 df-xp 
 |-  ( A X. _V ) = { <. x , y >. | ( x e. A /\ y e. _V ) }
3 vex 
 |-  y e. _V
4 3 biantru 
 |-  ( x e. A <-> ( x e. A /\ y e. _V ) )
5 4 opabbii 
 |-  { <. x , y >. | x e. A } = { <. x , y >. | ( x e. A /\ y e. _V ) }
6 2 5 eqtr4i 
 |-  ( A X. _V ) = { <. x , y >. | x e. A }
7 6 ineq2i 
 |-  ( { <. x , y >. | ph } i^i ( A X. _V ) ) = ( { <. x , y >. | ph } i^i { <. x , y >. | x e. A } )
8 incom 
 |-  ( { <. x , y >. | ph } i^i { <. x , y >. | x e. A } ) = ( { <. x , y >. | x e. A } i^i { <. x , y >. | ph } )
9 7 8 eqtri 
 |-  ( { <. x , y >. | ph } i^i ( A X. _V ) ) = ( { <. x , y >. | x e. A } i^i { <. x , y >. | ph } )
10 inopab 
 |-  ( { <. x , y >. | x e. A } i^i { <. x , y >. | ph } ) = { <. x , y >. | ( x e. A /\ ph ) }
11 9 10 eqtri 
 |-  ( { <. x , y >. | ph } i^i ( A X. _V ) ) = { <. x , y >. | ( x e. A /\ ph ) }
12 1 11 eqtri 
 |-  ( { <. x , y >. | ph } |` A ) = { <. x , y >. | ( x e. A /\ ph ) }