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 ) )