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