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 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) = 𝐵 )