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 𝐴 ∈ V
eufnfv.2 𝐵 ∈ V
Assertion eufnfv ∃! 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥𝐴 ( 𝑓𝑥 ) = 𝐵 )

Proof

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