Theorem fvopab6

Description: Value of a function given by ordered-pair class abstraction. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 11-Sep-2015)

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

Proof

Step	Hyp	Ref	Expression
1		fvopab6.1	|- F = { <. x , y >. | ( ph /\ y = B ) }
2		fvopab6.2	|- ( x = A -> ( ph <-> ps ) )
3		fvopab6.3	|- ( x = A -> B = C )
4		elex	|- ( A e. D -> A e. _V )
5	3	eqeq2d	|- ( x = A -> ( y = B <-> y = C ) )
6	2 5	anbi12d	|- ( x = A -> ( ( ph /\ y = B ) <-> ( ps /\ y = C ) ) )
7		iba	|- ( y = C -> ( ps <-> ( ps /\ y = C ) ) )
8	7	bicomd	|- ( y = C -> ( ( ps /\ y = C ) <-> ps ) )
9		moeq	|- E* y y = B
10	9	moani	|- E* y ( ph /\ y = B )
11	10	a1i	|- ( x e. _V -> E* y ( ph /\ y = B ) )
12		vex	|- x e. _V
13	12	biantrur	|- ( ( ph /\ y = B ) <-> ( x e. _V /\ ( ph /\ y = B ) ) )
14	13	opabbii	|- { <. x , y >. | ( ph /\ y = B ) } = { <. x , y >. | ( x e. _V /\ ( ph /\ y = B ) ) }
15	1 14	eqtri	|- F = { <. x , y >. | ( x e. _V /\ ( ph /\ y = B ) ) }
16	6 8 11 15	fvopab3ig	|- ( ( A e. _V /\ C e. R ) -> ( ps -> ( F ` A ) = C ) )
17	4 16	sylan	|- ( ( A e. D /\ C e. R ) -> ( ps -> ( F ` A ) = C ) )
18	17	3impia	|- ( ( A e. D /\ C e. R /\ ps ) -> ( F ` A ) = C )