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

Step	Hyp	Ref	Expression
1		tz6.12f.1	$⊢ \underline{Ⅎ} y F$
2		opeq2	$⊢ z = y \to ⟨A, z⟩ = ⟨A, y⟩$
3	2	eleq1d	$⊢ z = y \to (⟨A, z⟩ \in F \leftrightarrow ⟨A, y⟩ \in F)$
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 (\exists! z ⟨A, z⟩ \in F \leftrightarrow \exists! y ⟨A, y⟩ \in F)$
8	3 7	anbi12d	$⊢ z = y \to ((⟨A, z⟩ \in F \land \exists! z ⟨A, z⟩ \in F) \leftrightarrow (⟨A, y⟩ \in F \land \exists! y ⟨A, y⟩ \in F))$
9		eqeq2	$⊢ z = y \to (F (A) = z \leftrightarrow F (A) = y)$
10	8 9	imbi12d	$⊢ z = y \to (((⟨A, z⟩ \in F \land \exists! z ⟨A, z⟩ \in F) \to F (A) = z) \leftrightarrow ((⟨A, y⟩ \in F \land \exists! y ⟨A, y⟩ \in F) \to F (A) = y))$
11		tz6.12	$⊢ (⟨A, z⟩ \in F \land \exists! z ⟨A, z⟩ \in F) \to F (A) = z$
12	10 11	chvarvv	$⊢ (⟨A, y⟩ \in F \land \exists! y ⟨A, y⟩ \in F) \to F (A) = y$

Metamath Proof Explorer