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 
|- ( ph -> M Fn A )
fnmptfvd.s 
|- ( i = a -> D = C )
fnmptfvd.d 
|- ( ( ph /\ i e. A ) -> D e. U )
fnmptfvd.c 
|- ( ( ph /\ a e. A ) -> C e. V )
Assertion fnmptfvd 
|- ( ph -> ( M = ( a e. A |-> C ) <-> A. i e. A ( M ` i ) = D ) )

Proof

Step Hyp Ref Expression
1 fnmptfvd.m 
 |-  ( ph -> M Fn A )
2 fnmptfvd.s 
 |-  ( i = a -> D = C )
3 fnmptfvd.d 
 |-  ( ( ph /\ i e. A ) -> D e. U )
4 fnmptfvd.c 
 |-  ( ( ph /\ a e. A ) -> C e. V )
5 4 ralrimiva 
 |-  ( ph -> A. a e. A C e. V )
6 eqid 
 |-  ( a e. A |-> C ) = ( a e. A |-> C )
7 6 fnmpt 
 |-  ( A. a e. A C e. V -> ( a e. A |-> C ) Fn A )
8 5 7 syl 
 |-  ( ph -> ( a e. A |-> C ) Fn A )
9 eqfnfv 
 |-  ( ( M Fn A /\ ( a e. A |-> C ) Fn A ) -> ( M = ( a e. A |-> C ) <-> A. i e. A ( M ` i ) = ( ( a e. A |-> C ) ` i ) ) )
10 1 8 9 syl2anc 
 |-  ( ph -> ( M = ( a e. A |-> C ) <-> A. i e. A ( M ` i ) = ( ( a e. A |-> C ) ` i ) ) )
11 2 cbvmptv 
 |-  ( i e. A |-> D ) = ( a e. A |-> C )
12 11 eqcomi 
 |-  ( a e. A |-> C ) = ( i e. A |-> D )
13 12 a1i 
 |-  ( ph -> ( a e. A |-> C ) = ( i e. A |-> D ) )
14 13 fveq1d 
 |-  ( ph -> ( ( a e. A |-> C ) ` i ) = ( ( i e. A |-> D ) ` i ) )
15 14 eqeq2d 
 |-  ( ph -> ( ( M ` i ) = ( ( a e. A |-> C ) ` i ) <-> ( M ` i ) = ( ( i e. A |-> D ) ` i ) ) )
16 15 ralbidv 
 |-  ( ph -> ( A. i e. A ( M ` i ) = ( ( a e. A |-> C ) ` i ) <-> A. i e. A ( M ` i ) = ( ( i e. A |-> D ) ` i ) ) )
17 simpr 
 |-  ( ( ph /\ i e. A ) -> i e. A )
18 eqid 
 |-  ( i e. A |-> D ) = ( i e. A |-> D )
19 18 fvmpt2 
 |-  ( ( i e. A /\ D e. U ) -> ( ( i e. A |-> D ) ` i ) = D )
20 17 3 19 syl2anc 
 |-  ( ( ph /\ i e. A ) -> ( ( i e. A |-> D ) ` i ) = D )
21 20 eqeq2d 
 |-  ( ( ph /\ i e. A ) -> ( ( M ` i ) = ( ( i e. A |-> D ) ` i ) <-> ( M ` i ) = D ) )
22 21 ralbidva 
 |-  ( ph -> ( A. i e. A ( M ` i ) = ( ( i e. A |-> D ) ` i ) <-> A. i e. A ( M ` i ) = D ) )
23 10 16 22 3bitrd 
 |-  ( ph -> ( M = ( a e. A |-> C ) <-> A. i e. A ( M ` i ) = D ) )