Metamath Proof Explorer

Theorem resoprab2

Description: Restriction of an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009)

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

Proof

Step Hyp Ref Expression
1 resoprab 
 |-  ( { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) } |` ( C X. D ) ) = { <. <. x , y >. , z >. | ( ( x e. C /\ y e. D ) /\ ( ( x e. A /\ y e. B ) /\ ph ) ) }
2 anass 
 |-  ( ( ( ( x e. C /\ y e. D ) /\ ( x e. A /\ y e. B ) ) /\ ph ) <-> ( ( x e. C /\ y e. D ) /\ ( ( x e. A /\ y e. B ) /\ ph ) ) )
3 an4 
 |-  ( ( ( x e. C /\ y e. D ) /\ ( x e. A /\ y e. B ) ) <-> ( ( x e. C /\ x e. A ) /\ ( y e. D /\ y e. B ) ) )
4 ssel 
 |-  ( C C_ A -> ( x e. C -> x e. A ) )
5 4 pm4.71d 
 |-  ( C C_ A -> ( x e. C <-> ( x e. C /\ x e. A ) ) )
6 5 bicomd 
 |-  ( C C_ A -> ( ( x e. C /\ x e. A ) <-> x e. C ) )
7 ssel 
 |-  ( D C_ B -> ( y e. D -> y e. B ) )
8 7 pm4.71d 
 |-  ( D C_ B -> ( y e. D <-> ( y e. D /\ y e. B ) ) )
9 8 bicomd 
 |-  ( D C_ B -> ( ( y e. D /\ y e. B ) <-> y e. D ) )
10 6 9 bi2anan9 
 |-  ( ( C C_ A /\ D C_ B ) -> ( ( ( x e. C /\ x e. A ) /\ ( y e. D /\ y e. B ) ) <-> ( x e. C /\ y e. D ) ) )
11 3 10 syl5bb 
 |-  ( ( C C_ A /\ D C_ B ) -> ( ( ( x e. C /\ y e. D ) /\ ( x e. A /\ y e. B ) ) <-> ( x e. C /\ y e. D ) ) )
12 11 anbi1d 
 |-  ( ( C C_ A /\ D C_ B ) -> ( ( ( ( x e. C /\ y e. D ) /\ ( x e. A /\ y e. B ) ) /\ ph ) <-> ( ( x e. C /\ y e. D ) /\ ph ) ) )
13 2 12 bitr3id 
 |-  ( ( C C_ A /\ D C_ B ) -> ( ( ( x e. C /\ y e. D ) /\ ( ( x e. A /\ y e. B ) /\ ph ) ) <-> ( ( x e. C /\ y e. D ) /\ ph ) ) )
14 13 oprabbidv 
 |-  ( ( C C_ A /\ D C_ B ) -> { <. <. x , y >. , z >. | ( ( x e. C /\ y e. D ) /\ ( ( x e. A /\ y e. B ) /\ ph ) ) } = { <. <. x , y >. , z >. | ( ( x e. C /\ y e. D ) /\ ph ) } )
15 1 14 syl5eq 
 |-  ( ( C C_ A /\ D C_ B ) -> ( { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ ph ) } |` ( C X. D ) ) = { <. <. x , y >. , z >. | ( ( x e. C /\ y e. D ) /\ ph ) } )