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	$$⊢\underset{\_}{Ⅎ}yF$$
Assertion	tz6.12f	$$⊢\left(⟨A,y⟩\in F\wedge \exists !y⟨A,y⟩\in F\right)\to F\left(A\right)=y$$

Proof

Step	Hyp	Ref	Expression
1		tz6.12f.1	$$⊢\underset{\_}{Ⅎ}yF$$
2		opeq2	$$⊢z=y\to ⟨A,z⟩=⟨A,y⟩$$
3	2	eleq1d	$$⊢z=y\to \left(⟨A,z⟩\in F\leftrightarrow ⟨A,y⟩\in F\right)$$
4	1	nfel2	$$⊢Ⅎy⟨A,z⟩\in F$$
5		nfv	$$⊢Ⅎz⟨A,y⟩\in F$$
6	4 5 3	cbveuw	$$⊢\exists !z⟨A,z⟩\in F\leftrightarrow \exists !y⟨A,y⟩\in F$$
7	6	a1i	$$⊢z=y\to \left(\exists !z⟨A,z⟩\in F\leftrightarrow \exists !y⟨A,y⟩\in F\right)$$
8	3 7	anbi12d	$$⊢z=y\to \left(\left(⟨A,z⟩\in F\wedge \exists !z⟨A,z⟩\in F\right)\leftrightarrow \left(⟨A,y⟩\in F\wedge \exists !y⟨A,y⟩\in F\right)\right)$$
9		eqeq2	$$⊢z=y\to \left(F\left(A\right)=z\leftrightarrow F\left(A\right)=y\right)$$
10	8 9	imbi12d	$$⊢z=y\to \left(\left(\left(⟨A,z⟩\in F\wedge \exists !z⟨A,z⟩\in F\right)\to F\left(A\right)=z\right)\leftrightarrow \left(\left(⟨A,y⟩\in F\wedge \exists !y⟨A,y⟩\in F\right)\to F\left(A\right)=y\right)\right)$$
11		tz6.12	$$⊢\left(⟨A,z⟩\in F\wedge \exists !z⟨A,z⟩\in F\right)\to F\left(A\right)=z$$
12	10 11	chvarvv	$$⊢\left(⟨A,y⟩\in F\wedge \exists !y⟨A,y⟩\in F\right)\to F\left(A\right)=y$$