Step |
Hyp |
Ref |
Expression |
1 |
|
opelopabga.1 |
|- ( ( x = A /\ y = B ) -> ( ph <-> ps ) ) |
2 |
|
eleq1 |
|- ( x = A -> ( x e. C <-> A e. C ) ) |
3 |
|
eleq1 |
|- ( y = B -> ( y e. D <-> B e. D ) ) |
4 |
2 3
|
bi2anan9 |
|- ( ( x = A /\ y = B ) -> ( ( x e. C /\ y e. D ) <-> ( A e. C /\ B e. D ) ) ) |
5 |
4 1
|
anbi12d |
|- ( ( x = A /\ y = B ) -> ( ( ( x e. C /\ y e. D ) /\ ph ) <-> ( ( A e. C /\ B e. D ) /\ ps ) ) ) |
6 |
5
|
opelopabga |
|- ( ( A e. C /\ B e. D ) -> ( <. A , B >. e. { <. x , y >. | ( ( x e. C /\ y e. D ) /\ ph ) } <-> ( ( A e. C /\ B e. D ) /\ ps ) ) ) |
7 |
6
|
bianabs |
|- ( ( A e. C /\ B e. D ) -> ( <. A , B >. e. { <. x , y >. | ( ( x e. C /\ y e. D ) /\ ph ) } <-> ps ) ) |