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 )