Theorem fvopab5 6309

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

Hypotheses

Ref	Expression
fvopab5.1	|- F = { <. x , y >. | ph }
fvopab5.2	|- ( x = A -> ( ph <-> ps ) )

Assertion

Ref	Expression
fvopab5	|- ( A e. V -> ( F ` A ) = ( iota y ps ) )

Distinct variable groups:   x, y, A   ps, x

Allowed substitution hints:   ph( x, y)   ps( y)   F( x, y)   V( x, y)

Proof of Theorem fvopab5

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 3212	. 2 |- ( A e. V -> A e. _V )
2		df-fv 5896	. . . 4 |- ( F ` A ) = ( iota z A F z )
3		breq2 4657	. . . . 5 |- ( z = y -> ( A F z <-> A F y ) )
4		nfcv 2764	. . . . . 6 |- F/_ y A
5		fvopab5.1	. . . . . . 7 |- F = { <. x , y >. | ph }
6		nfopab2 4720	. . . . . . 7 |- F/_ y { <. x , y >. | ph }
7	5, 6	nfcxfr 2762	. . . . . 6 |- F/_ y F
8		nfcv 2764	. . . . . 6 |- F/_ y z
9	4, 7, 8	nfbr 4699	. . . . 5 |- F/ y A F z
10		nfv 1843	. . . . 5 |- F/ z A F y
11	3, 9, 10	cbviota 5856	. . . 4 |- ( iota z A F z ) = ( iota y A F y )
12	2, 11	eqtri 2644	. . 3 |- ( F ` A ) = ( iota y A F y )
13		nfcv 2764	. . . . . . 7 |- F/_ x A
14		nfopab1 4719	. . . . . . . 8 |- F/_ x { <. x , y >. | ph }
15	5, 14	nfcxfr 2762	. . . . . . 7 |- F/_ x F
16		nfcv 2764	. . . . . . 7 |- F/_ x y
17	13, 15, 16	nfbr 4699	. . . . . 6 |- F/ x A F y
18		nfv 1843	. . . . . 6 |- F/ x ps
19	17, 18	nfbi 1833	. . . . 5 |- F/ x ( A F y <-> ps )
20		breq1 4656	. . . . . 6 |- ( x = A -> ( x F y <-> A F y ) )
21		fvopab5.2	. . . . . 6 |- ( x = A -> ( ph <-> ps ) )
22	20, 21	bibi12d 335	. . . . 5 |- ( x = A -> ( ( x F y <-> ph ) <-> ( A F y <-> ps ) ) )
23		df-br 4654	. . . . . 6 |- ( x F y <-> <. x , y >. e. F )
24	5	eleq2i 2693	. . . . . 6 |- ( <. x , y >. e. F <-> <. x , y >. e. { <. x , y >. | ph } )
25		opabid 4982	. . . . . 6 |- ( <. x , y >. e. { <. x , y >. | ph } <-> ph )
26	23, 24, 25	3bitri 286	. . . . 5 |- ( x F y <-> ph )
27	19, 22, 26	vtoclg1f 3265	. . . 4 |- ( A e. _V -> ( A F y <-> ps ) )
28	27	iotabidv 5872	. . 3 |- ( A e. _V -> ( iota y A F y ) = ( iota y ps ) )
29	12, 28	syl5eq 2668	. 2 |- ( A e. _V -> ( F ` A ) = ( iota y ps ) )
30	1, 29	syl 17	1 |- ( A e. V -> ( F ` A ) = ( iota y ps ) )

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   e. wcel 1990   _Vcvv 3200   <.cop 4183   class class class wbr 4653   {copab 4712   iotacio 5849   ` cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-iota 5851  df-fv 5896

This theorem is referenced by:  ajval  27717  adjval  28749