This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fvopab3g

Description: Value of a function given by ordered-pair class abstraction. (Contributed by NM, 6-Mar-1996) (Revised by Mario Carneiro, 28-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 fvopab3g.2 
 |-  ( x = A -> ( ph <-> ps ) )
2 fvopab3g.3 
 |-  ( y = B -> ( ps <-> ch ) )
3 fvopab3g.4 
 |-  ( x e. C -> E! y ph )
4 fvopab3g.5 
 |-  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 3 4 fnopab 
 |-  F Fn C
10 fnopfvb 
 |-  ( ( F Fn C /\ A e. C ) -> ( ( F ` A ) = B <-> <. A , B >. e. F ) )
11 9 10 mpan 
 |-  ( A e. C -> ( ( F ` A ) = B <-> <. A , B >. e. F ) )
12 4 eleq2i 
 |-  ( <. A , B >. e. F <-> <. A , B >. e. { <. x , y >. | ( x e. C /\ ph ) } )
13 11 12 bitrdi 
 |-  ( A e. C -> ( ( F ` A ) = B <-> <. A , B >. e. { <. x , y >. | ( x e. C /\ ph ) } ) )
14 13 adantr 
 |-  ( ( A e. C /\ B e. D ) -> ( ( F ` A ) = B <-> <. A , B >. e. { <. x , y >. | ( x e. C /\ ph ) } ) )
15 ibar 
 |-  ( A e. C -> ( ch <-> ( A e. C /\ ch ) ) )
16 15 adantr 
 |-  ( ( A e. C /\ B e. D ) -> ( ch <-> ( A e. C /\ ch ) ) )
17 8 14 16 3bitr4d 
 |-  ( ( A e. C /\ B e. D ) -> ( ( F ` A ) = B <-> ch ) )