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 syl5eq 
 |-  ( <. 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 ) )