Metamath Proof Explorer

Theorem fnmptfvd

Description: A function with a given domain is a mapping defined by its function values. (Contributed by AV, 1-Mar-2019)

Ref Expression
Hypotheses fnmptfvd.m ⊢ φ → M Fn A
fnmptfvd.s ⊢ i = a → D = C
fnmptfvd.d ⊢ φ ∧ i ∈ A → D ∈ U
fnmptfvd.c ⊢ φ ∧ a ∈ A → C ∈ V
Assertion fnmptfvd ⊢ φ → M = a ∈ A ⟼ C ↔ ∀ i ∈ A M ⁡ i = D

Proof

Step Hyp Ref Expression
1 fnmptfvd.m ⊢ φ → M Fn A
2 fnmptfvd.s ⊢ i = a → D = C
3 fnmptfvd.d ⊢ φ ∧ i ∈ A → D ∈ U
4 fnmptfvd.c ⊢ φ ∧ a ∈ A → C ∈ V
5 4 ralrimiva ⊢ φ → ∀ a ∈ A C ∈ V
6 eqid ⊢ a ∈ A ⟼ C = a ∈ A ⟼ C
7 6 fnmpt ⊢ ∀ a ∈ A C ∈ V → a ∈ A ⟼ C Fn A
8 5 7 syl ⊢ φ → a ∈ A ⟼ C Fn A
9 eqfnfv ⊢ M Fn A ∧ a ∈ A ⟼ C Fn A → M = a ∈ A ⟼ C ↔ ∀ i ∈ A M ⁡ i = a ∈ A ⟼ C ⁡ i
10 1 8 9 syl2anc ⊢ φ → M = a ∈ A ⟼ C ↔ ∀ i ∈ A M ⁡ i = a ∈ A ⟼ C ⁡ i
11 2 cbvmptv ⊢ i ∈ A ⟼ D = a ∈ A ⟼ C
12 11 eqcomi ⊢ a ∈ A ⟼ C = i ∈ A ⟼ D
13 12 a1i ⊢ φ → a ∈ A ⟼ C = i ∈ A ⟼ D
14 13 fveq1d ⊢ φ → a ∈ A ⟼ C ⁡ i = i ∈ A ⟼ D ⁡ i
15 14 eqeq2d ⊢ φ → M ⁡ i = a ∈ A ⟼ C ⁡ i ↔ M ⁡ i = i ∈ A ⟼ D ⁡ i
16 15 ralbidv ⊢ φ → ∀ i ∈ A M ⁡ i = a ∈ A ⟼ C ⁡ i ↔ ∀ i ∈ A M ⁡ i = i ∈ A ⟼ D ⁡ i
17 simpr ⊢ φ ∧ i ∈ A → i ∈ A
18 eqid ⊢ i ∈ A ⟼ D = i ∈ A ⟼ D
19 18 fvmpt2 ⊢ i ∈ A ∧ D ∈ U → i ∈ A ⟼ D ⁡ i = D
20 17 3 19 syl2anc ⊢ φ ∧ i ∈ A → i ∈ A ⟼ D ⁡ i = D
21 20 eqeq2d ⊢ φ ∧ i ∈ A → M ⁡ i = i ∈ A ⟼ D ⁡ i ↔ M ⁡ i = D
22 21 ralbidva ⊢ φ → ∀ i ∈ A M ⁡ i = i ∈ A ⟼ D ⁡ i ↔ ∀ i ∈ A M ⁡ i = D
23 10 16 22 3bitrd ⊢ φ → M = a ∈ A ⟼ C ↔ ∀ i ∈ A M ⁡ i = D