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 ) } )