Metamath Proof Explorer


Theorem fvopab3ig

Description: Value of a function given by ordered-pair class abstraction. (Contributed by NM, 23-Oct-1999)

Ref Expression
Hypotheses fvopab3ig.1
|- ( x = A -> ( ph <-> ps ) )
fvopab3ig.2
|- ( y = B -> ( ps <-> ch ) )
fvopab3ig.3
|- ( x e. C -> E* y ph )
fvopab3ig.4
|- F = { <. x , y >. | ( x e. C /\ ph ) }
Assertion fvopab3ig
|- ( ( A e. C /\ B e. D ) -> ( ch -> ( F ` A ) = B ) )

Proof

Step Hyp Ref Expression
1 fvopab3ig.1
 |-  ( x = A -> ( ph <-> ps ) )
2 fvopab3ig.2
 |-  ( y = B -> ( ps <-> ch ) )
3 fvopab3ig.3
 |-  ( x e. C -> E* y ph )
4 fvopab3ig.4
 |-  F = { <. x , y >. | ( x e. C /\ ph ) }
5 eleq1
 |-  ( x = A -> ( x e. C <-> A e. C ) )
6 5 1 anbi12d
 |-  ( x = A -> ( ( x e. C /\ ph ) <-> ( A e. C /\ ps ) ) )
7 2 anbi2d
 |-  ( y = B -> ( ( A e. C /\ ps ) <-> ( A e. C /\ ch ) ) )
8 6 7 opelopabg
 |-  ( ( A e. C /\ B e. D ) -> ( <. A , B >. e. { <. x , y >. | ( x e. C /\ ph ) } <-> ( A e. C /\ ch ) ) )
9 8 biimpar
 |-  ( ( ( A e. C /\ B e. D ) /\ ( A e. C /\ ch ) ) -> <. A , B >. e. { <. x , y >. | ( x e. C /\ ph ) } )
10 9 exp43
 |-  ( A e. C -> ( B e. D -> ( A e. C -> ( ch -> <. A , B >. e. { <. x , y >. | ( x e. C /\ ph ) } ) ) ) )
11 10 pm2.43a
 |-  ( A e. C -> ( B e. D -> ( ch -> <. A , B >. e. { <. x , y >. | ( x e. C /\ ph ) } ) ) )
12 11 imp
 |-  ( ( A e. C /\ B e. D ) -> ( ch -> <. A , B >. e. { <. x , y >. | ( x e. C /\ ph ) } ) )
13 4 fveq1i
 |-  ( F ` A ) = ( { <. x , y >. | ( x e. C /\ ph ) } ` A )
14 funopab
 |-  ( Fun { <. x , y >. | ( x e. C /\ ph ) } <-> A. x E* y ( x e. C /\ ph ) )
15 moanimv
 |-  ( E* y ( x e. C /\ ph ) <-> ( x e. C -> E* y ph ) )
16 3 15 mpbir
 |-  E* y ( x e. C /\ ph )
17 14 16 mpgbir
 |-  Fun { <. x , y >. | ( x e. C /\ ph ) }
18 funopfv
 |-  ( Fun { <. x , y >. | ( x e. C /\ ph ) } -> ( <. A , B >. e. { <. x , y >. | ( x e. C /\ ph ) } -> ( { <. x , y >. | ( x e. C /\ ph ) } ` A ) = B ) )
19 17 18 ax-mp
 |-  ( <. A , B >. e. { <. x , y >. | ( x e. C /\ ph ) } -> ( { <. x , y >. | ( x e. C /\ ph ) } ` A ) = B )
20 13 19 eqtrid
 |-  ( <. A , B >. e. { <. x , y >. | ( x e. C /\ ph ) } -> ( F ` A ) = B )
21 12 20 syl6
 |-  ( ( A e. C /\ B e. D ) -> ( ch -> ( F ` A ) = B ) )