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	⊢ Ⅎ 𝑦 𝐹
Assertion	tz6.12f	⊢ ( ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ∧ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) → ( 𝐹 ‘ 𝐴 ) = 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		tz6.12f.1	⊢ Ⅎ 𝑦 𝐹
2		opeq2	⊢ ( 𝑧 = 𝑦 → ⟨ 𝐴 , 𝑧 ⟩ = ⟨ 𝐴 , 𝑦 ⟩ )
3	2	eleq1d	⊢ ( 𝑧 = 𝑦 → ( ⟨ 𝐴 , 𝑧 ⟩ ∈ 𝐹 ↔ ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) )
4	1	nfel2	⊢ Ⅎ 𝑦 ⟨ 𝐴 , 𝑧 ⟩ ∈ 𝐹
5		nfv	⊢ Ⅎ 𝑧 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹
6	4 5 3	cbveuw	⊢ ( ∃! 𝑧 ⟨ 𝐴 , 𝑧 ⟩ ∈ 𝐹 ↔ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 )
7	6	a1i	⊢ ( 𝑧 = 𝑦 → ( ∃! 𝑧 ⟨ 𝐴 , 𝑧 ⟩ ∈ 𝐹 ↔ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) )
8	3 7	anbi12d	⊢ ( 𝑧 = 𝑦 → ( ( ⟨ 𝐴 , 𝑧 ⟩ ∈ 𝐹 ∧ ∃! 𝑧 ⟨ 𝐴 , 𝑧 ⟩ ∈ 𝐹 ) ↔ ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ∧ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) ) )
9		eqeq2	⊢ ( 𝑧 = 𝑦 → ( ( 𝐹 ‘ 𝐴 ) = 𝑧 ↔ ( 𝐹 ‘ 𝐴 ) = 𝑦 ) )
10	8 9	imbi12d	⊢ ( 𝑧 = 𝑦 → ( ( ( ⟨ 𝐴 , 𝑧 ⟩ ∈ 𝐹 ∧ ∃! 𝑧 ⟨ 𝐴 , 𝑧 ⟩ ∈ 𝐹 ) → ( 𝐹 ‘ 𝐴 ) = 𝑧 ) ↔ ( ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ∧ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) → ( 𝐹 ‘ 𝐴 ) = 𝑦 ) ) )
11		tz6.12	⊢ ( ( ⟨ 𝐴 , 𝑧 ⟩ ∈ 𝐹 ∧ ∃! 𝑧 ⟨ 𝐴 , 𝑧 ⟩ ∈ 𝐹 ) → ( 𝐹 ‘ 𝐴 ) = 𝑧 )
12	10 11	chvarvv	⊢ ( ( ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ∧ ∃! 𝑦 ⟨ 𝐴 , 𝑦 ⟩ ∈ 𝐹 ) → ( 𝐹 ‘ 𝐴 ) = 𝑦 )