Theorem tz6.12f 5443

Description: Function value, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 30-Aug-1999.)

Hypothesis

Ref	Expression
tz6.12f.1	⊢ Ⅎ𝑦𝐹

Assertion

Ref	Expression
tz6.12f	⊢ ((⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦⟨𝐴, 𝑦⟩ ∈ 𝐹) → (𝐹‘𝐴) = 𝑦)

Distinct variable group:   𝑦,𝐴

Allowed substitution hint:   𝐹(𝑦)

Proof of Theorem tz6.12f

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		opeq2 3701	. . . . 5 ⊢ (𝑧 = 𝑦 → ⟨𝐴, 𝑧⟩ = ⟨𝐴, 𝑦⟩)
2	1	eleq1d 2206	. . . 4 ⊢ (𝑧 = 𝑦 → (⟨𝐴, 𝑧⟩ ∈ 𝐹 ↔ ⟨𝐴, 𝑦⟩ ∈ 𝐹))
3		tz6.12f.1	. . . . . . 7 ⊢ Ⅎ𝑦𝐹
4	3	nfel2 2292	. . . . . 6 ⊢ Ⅎ𝑦⟨𝐴, 𝑧⟩ ∈ 𝐹
5		nfv 1508	. . . . . 6 ⊢ Ⅎ𝑧⟨𝐴, 𝑦⟩ ∈ 𝐹
6	4, 5, 2	cbveu 2021	. . . . 5 ⊢ (∃!𝑧⟨𝐴, 𝑧⟩ ∈ 𝐹 ↔ ∃!𝑦⟨𝐴, 𝑦⟩ ∈ 𝐹)
7	6	a1i 9	. . . 4 ⊢ (𝑧 = 𝑦 → (∃!𝑧⟨𝐴, 𝑧⟩ ∈ 𝐹 ↔ ∃!𝑦⟨𝐴, 𝑦⟩ ∈ 𝐹))
8	2, 7	anbi12d 464	. . 3 ⊢ (𝑧 = 𝑦 → ((⟨𝐴, 𝑧⟩ ∈ 𝐹 ∧ ∃!𝑧⟨𝐴, 𝑧⟩ ∈ 𝐹) ↔ (⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦⟨𝐴, 𝑦⟩ ∈ 𝐹)))
9		eqeq2 2147	. . 3 ⊢ (𝑧 = 𝑦 → ((𝐹‘𝐴) = 𝑧 ↔ (𝐹‘𝐴) = 𝑦))
10	8, 9	imbi12d 233	. 2 ⊢ (𝑧 = 𝑦 → (((⟨𝐴, 𝑧⟩ ∈ 𝐹 ∧ ∃!𝑧⟨𝐴, 𝑧⟩ ∈ 𝐹) → (𝐹‘𝐴) = 𝑧) ↔ ((⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦⟨𝐴, 𝑦⟩ ∈ 𝐹) → (𝐹‘𝐴) = 𝑦)))
11		tz6.12 5442	. 2 ⊢ ((⟨𝐴, 𝑧⟩ ∈ 𝐹 ∧ ∃!𝑧⟨𝐴, 𝑧⟩ ∈ 𝐹) → (𝐹‘𝐴) = 𝑧)
12	10, 11	chvarv 1907	1 ⊢ ((⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦⟨𝐴, 𝑦⟩ ∈ 𝐹) → (𝐹‘𝐴) = 𝑦)

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1331   ∈ wcel 1480  ∃!weu 1997  Ⅎwnfc 2266  ⟨cop 3525  ‘cfv 5118

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-eu 2000  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-rex 2420  df-v 2683  df-sbc 2905  df-un 3070  df-sn 3528  df-pr 3529  df-op 3531  df-uni 3732  df-br 3925  df-iota 5083  df-fv 5126

This theorem is referenced by: (None)