Metamath Proof Explorer

Theorem eufnfv

Description: A function is uniquely determined by its values. (Contributed by NM, 31-Aug-2011)

Ref Expression
Hypotheses eufnfv.1 ⊢ A ∈ V
eufnfv.2 ⊢ B ∈ V
Assertion eufnfv ⊢ ∃! f f Fn A ∧ ∀ x ∈ A f ⁡ x = B

Proof

Step Hyp Ref Expression
1 eufnfv.1 ⊢ A ∈ V
2 eufnfv.2 ⊢ B ∈ V
3 1 mptex ⊢ x ∈ A ⟼ B ∈ V
4 eqeq2 ⊢ z = x ∈ A ⟼ B → f = z ↔ f = x ∈ A ⟼ B
5 4 bibi2d ⊢ z = x ∈ A ⟼ B → f Fn A ∧ ∀ x ∈ A f ⁡ x = B ↔ f = z ↔ f Fn A ∧ ∀ x ∈ A f ⁡ x = B ↔ f = x ∈ A ⟼ B
6 5 albidv ⊢ z = x ∈ A ⟼ B → ∀ f f Fn A ∧ ∀ x ∈ A f ⁡ x = B ↔ f = z ↔ ∀ f f Fn A ∧ ∀ x ∈ A f ⁡ x = B ↔ f = x ∈ A ⟼ B
7 3 6 spcev ⊢ ∀ f f Fn A ∧ ∀ x ∈ A f ⁡ x = B ↔ f = x ∈ A ⟼ B → ∃ z ∀ f f Fn A ∧ ∀ x ∈ A f ⁡ x = B ↔ f = z
8 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
9 2 8 fnmpti ⊢ x ∈ A ⟼ B Fn A
10 fneq1 ⊢ f = x ∈ A ⟼ B → f Fn A ↔ x ∈ A ⟼ B Fn A
11 9 10 mpbiri ⊢ f = x ∈ A ⟼ B → f Fn A
12 11 pm4.71ri ⊢ f = x ∈ A ⟼ B ↔ f Fn A ∧ f = x ∈ A ⟼ B
13 dffn5 ⊢ f Fn A ↔ f = x ∈ A ⟼ f ⁡ x
14 eqeq1 ⊢ f = x ∈ A ⟼ f ⁡ x → f = x ∈ A ⟼ B ↔ x ∈ A ⟼ f ⁡ x = x ∈ A ⟼ B
15 13 14 sylbi ⊢ f Fn A → f = x ∈ A ⟼ B ↔ x ∈ A ⟼ f ⁡ x = x ∈ A ⟼ B
16 fvex ⊢ f ⁡ x ∈ V
17 16 rgenw ⊢ ∀ x ∈ A f ⁡ x ∈ V
18 mpteqb ⊢ ∀ x ∈ A f ⁡ x ∈ V → x ∈ A ⟼ f ⁡ x = x ∈ A ⟼ B ↔ ∀ x ∈ A f ⁡ x = B
19 17 18 ax-mp ⊢ x ∈ A ⟼ f ⁡ x = x ∈ A ⟼ B ↔ ∀ x ∈ A f ⁡ x = B
20 15 19 bitrdi ⊢ f Fn A → f = x ∈ A ⟼ B ↔ ∀ x ∈ A f ⁡ x = B
21 20 pm5.32i ⊢ f Fn A ∧ f = x ∈ A ⟼ B ↔ f Fn A ∧ ∀ x ∈ A f ⁡ x = B
22 12 21 bitr2i ⊢ f Fn A ∧ ∀ x ∈ A f ⁡ x = B ↔ f = x ∈ A ⟼ B
23 7 22 mpg ⊢ ∃ z ∀ f f Fn A ∧ ∀ x ∈ A f ⁡ x = B ↔ f = z
24 eu6 ⊢ ∃! f f Fn A ∧ ∀ x ∈ A f ⁡ x = B ↔ ∃ z ∀ f f Fn A ∧ ∀ x ∈ A f ⁡ x = B ↔ f = z
25 23 24 mpbir ⊢ ∃! f f Fn A ∧ ∀ x ∈ A f ⁡ x = B