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 ⊢∃!ffFnA∧∀x∈Af⁡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→fFnA∧∀x∈Af⁡x=B↔f=z↔fFnA∧∀x∈Af⁡x=B↔f=x∈A⟼B
6 5 albidv ⊢z=x∈A⟼B→∀ffFnA∧∀x∈Af⁡x=B↔f=z↔∀ffFnA∧∀x∈Af⁡x=B↔f=x∈A⟼B
7 3 6 spcev ⊢∀ffFnA∧∀x∈Af⁡x=B↔f=x∈A⟼B→∃z∀ffFnA∧∀x∈Af⁡x=B↔f=z
8 eqid ⊢x∈A⟼B=x∈A⟼B
9 2 8 fnmpti ⊢x∈A⟼BFnA
10 fneq1 ⊢f=x∈A⟼B→fFnA↔x∈A⟼BFnA
11 9 10 mpbiri ⊢f=x∈A⟼B→fFnA
12 11 pm4.71ri ⊢f=x∈A⟼B↔fFnA∧f=x∈A⟼B
13 dffn5 ⊢fFnA↔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 ⊢fFnA→f=x∈A⟼B↔x∈A⟼f⁡x=x∈A⟼B
16 fvex ⊢f⁡x∈V
17 16 rgenw ⊢∀x∈Af⁡x∈V
18 mpteqb ⊢∀x∈Af⁡x∈V→x∈A⟼f⁡x=x∈A⟼B↔∀x∈Af⁡x=B
19 17 18 ax-mp ⊢x∈A⟼f⁡x=x∈A⟼B↔∀x∈Af⁡x=B
20 15 19 bitrdi ⊢fFnA→f=x∈A⟼B↔∀x∈Af⁡x=B
21 20 pm5.32i ⊢fFnA∧f=x∈A⟼B↔fFnA∧∀x∈Af⁡x=B
22 12 21 bitr2i ⊢fFnA∧∀x∈Af⁡x=B↔f=x∈A⟼B
23 7 22 mpg ⊢∃z∀ffFnA∧∀x∈Af⁡x=B↔f=z
24 eu6 ⊢∃!ffFnA∧∀x∈Af⁡x=B↔∃z∀ffFnA∧∀x∈Af⁡x=B↔f=z
25 23 24 mpbir ⊢∃!ffFnA∧∀x∈Af⁡x=B