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

Metamath Proof Explorer

Theorem tz6.12f

Description: Function value, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 30-Aug-1999)

Ref Expression
Hypothesis tz6.12f.1 
|- F/_ y F
Assertion tz6.12f 
|- ( ( <. A , y >. e. F /\ E! y <. A , y >. e. F ) -> ( F ` A ) = y )

Proof

Step Hyp Ref Expression
1 tz6.12f.1 
 |-  F/_ y F
2 opeq2 
 |-  ( z = y -> <. A , z >. = <. A , y >. )
3 2 eleq1d 
 |-  ( z = y -> ( <. A , z >. e. F <-> <. A , y >. e. F ) )
4 1 nfel2 
 |-  F/ y <. A , z >. e. F
5 nfv 
 |-  F/ z <. A , y >. e. F
6 4 5 3 cbveuw 
 |-  ( E! z <. A , z >. e. F <-> E! y <. A , y >. e. F )
7 6 a1i 
 |-  ( z = y -> ( E! z <. A , z >. e. F <-> E! y <. A , y >. e. F ) )
8 3 7 anbi12d 
 |-  ( z = y -> ( ( <. A , z >. e. F /\ E! z <. A , z >. e. F ) <-> ( <. A , y >. e. F /\ E! y <. A , y >. e. F ) ) )
9 eqeq2 
 |-  ( z = y -> ( ( F ` A ) = z <-> ( F ` A ) = y ) )
10 8 9 imbi12d 
 |-  ( z = y -> ( ( ( <. A , z >. e. F /\ E! z <. A , z >. e. F ) -> ( F ` A ) = z ) <-> ( ( <. A , y >. e. F /\ E! y <. A , y >. e. F ) -> ( F ` A ) = y ) ) )
11 tz6.12 
 |-  ( ( <. A , z >. e. F /\ E! z <. A , z >. e. F ) -> ( F ` A ) = z )
12 10 11 chvarvv 
 |-  ( ( <. A , y >. e. F /\ E! y <. A , y >. e. F ) -> ( F ` A ) = y )