Theorem fvopab5

Description: The value of a function that is expressed as an ordered pair abstraction. (Contributed by NM, 19-Feb-2006) (Revised by Mario Carneiro, 11-Sep-2015)

	Ref	Expression
Hypotheses	fvopab5.1	|- F = { <. x , y >. | ph }
	fvopab5.2	|- ( x = A -> ( ph <-> ps ) )
Assertion	fvopab5	|- ( A e. V -> ( F ` A ) = ( iota y ps ) )

Proof

Step	Hyp	Ref	Expression
1		fvopab5.1	|- F = { <. x , y >. | ph }
2		fvopab5.2	|- ( x = A -> ( ph <-> ps ) )
3		elex	|- ( A e. V -> A e. _V )
4		df-fv	|- ( F ` A ) = ( iota z A F z )
5		breq2	|- ( z = y -> ( A F z <-> A F y ) )
6		nfcv	|- F/_ y A
7		nfopab2	|- F/_ y { <. x , y >. | ph }
8	1 7	nfcxfr	|- F/_ y F
9		nfcv	|- F/_ y z
10	6 8 9	nfbr	|- F/ y A F z
11		nfv	|- F/ z A F y
12	5 10 11	cbviotaw	|- ( iota z A F z ) = ( iota y A F y )
13	4 12	eqtri	|- ( F ` A ) = ( iota y A F y )
14		nfcv	|- F/_ x A
15		nfopab1	|- F/_ x { <. x , y >. | ph }
16	1 15	nfcxfr	|- F/_ x F
17		nfcv	|- F/_ x y
18	14 16 17	nfbr	|- F/ x A F y
19		nfv	|- F/ x ps
20	18 19	nfbi	|- F/ x ( A F y <-> ps )
21		breq1	|- ( x = A -> ( x F y <-> A F y ) )
22	21 2	bibi12d	|- ( x = A -> ( ( x F y <-> ph ) <-> ( A F y <-> ps ) ) )
23		df-br	|- ( x F y <-> <. x , y >. e. F )
24	1	eleq2i	|- ( <. x , y >. e. F <-> <. x , y >. e. { <. x , y >. | ph } )
25		opabidw	|- ( <. x , y >. e. { <. x , y >. | ph } <-> ph )
26	23 24 25	3bitri	|- ( x F y <-> ph )
27	20 22 26	vtoclg1f	|- ( A e. _V -> ( A F y <-> ps ) )
28	27	iotabidv	|- ( A e. _V -> ( iota y A F y ) = ( iota y ps ) )
29	13 28	syl5eq	|- ( A e. _V -> ( F ` A ) = ( iota y ps ) )
30	3 29	syl	|- ( A e. V -> ( F ` A ) = ( iota y ps ) )