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

Metamath Proof Explorer

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 eqtrid 
 |-  ( A e. _V -> ( F ` A ) = ( iota y ps ) )
30 3 29 syl 
 |-  ( A e. V -> ( F ` A ) = ( iota y ps ) )