This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem resopab2

Description: Restriction of a class abstraction of ordered pairs. (Contributed by NM, 24-Aug-2007)

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

Proof

Step Hyp Ref Expression
1 resopab 
 |-  ( { <. x , y >. | ( x e. B /\ ph ) } |` A ) = { <. x , y >. | ( x e. A /\ ( x e. B /\ ph ) ) }
2 ssel 
 |-  ( A C_ B -> ( x e. A -> x e. B ) )
3 2 pm4.71d 
 |-  ( A C_ B -> ( x e. A <-> ( x e. A /\ x e. B ) ) )
4 3 anbi1d 
 |-  ( A C_ B -> ( ( x e. A /\ ph ) <-> ( ( x e. A /\ x e. B ) /\ ph ) ) )
5 anass 
 |-  ( ( ( x e. A /\ x e. B ) /\ ph ) <-> ( x e. A /\ ( x e. B /\ ph ) ) )
6 4 5 bitr2di 
 |-  ( A C_ B -> ( ( x e. A /\ ( x e. B /\ ph ) ) <-> ( x e. A /\ ph ) ) )
7 6 opabbidv 
 |-  ( A C_ B -> { <. x , y >. | ( x e. A /\ ( x e. B /\ ph ) ) } = { <. x , y >. | ( x e. A /\ ph ) } )
8 1 7 eqtrid 
 |-  ( A C_ B -> ( { <. x , y >. | ( x e. B /\ ph ) } |` A ) = { <. x , y >. | ( x e. A /\ ph ) } )