This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fvmptf

Description: Value of a function given by an ordered-pair class abstraction. This version of fvmptg uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 8-Nov-2005) (Revised by Mario Carneiro, 15-Oct-2016)

Ref Expression
Hypotheses fvmptf.1 
|- F/_ x A
fvmptf.2 
|- F/_ x C
fvmptf.3 
|- ( x = A -> B = C )
fvmptf.4 
|- F = ( x e. D |-> B )
Assertion fvmptf 
|- ( ( A e. D /\ C e. V ) -> ( F ` A ) = C )

Proof

Step Hyp Ref Expression
1 fvmptf.1 
 |-  F/_ x A
2 fvmptf.2 
 |-  F/_ x C
3 fvmptf.3 
 |-  ( x = A -> B = C )
4 fvmptf.4 
 |-  F = ( x e. D |-> B )
5 2 nfel1 
 |-  F/ x C e. _V
6 nfmpt1 
 |-  F/_ x ( x e. D |-> B )
7 4 6 nfcxfr 
 |-  F/_ x F
8 7 1 nffv 
 |-  F/_ x ( F ` A )
9 8 2 nfeq 
 |-  F/ x ( F ` A ) = C
10 5 9 nfim 
 |-  F/ x ( C e. _V -> ( F ` A ) = C )
11 3 eleq1d 
 |-  ( x = A -> ( B e. _V <-> C e. _V ) )
12 fveq2 
 |-  ( x = A -> ( F ` x ) = ( F ` A ) )
13 12 3 eqeq12d 
 |-  ( x = A -> ( ( F ` x ) = B <-> ( F ` A ) = C ) )
14 11 13 imbi12d 
 |-  ( x = A -> ( ( B e. _V -> ( F ` x ) = B ) <-> ( C e. _V -> ( F ` A ) = C ) ) )
15 4 fvmpt2 
 |-  ( ( x e. D /\ B e. _V ) -> ( F ` x ) = B )
16 15 ex 
 |-  ( x e. D -> ( B e. _V -> ( F ` x ) = B ) )
17 1 10 14 16 vtoclgaf 
 |-  ( A e. D -> ( C e. _V -> ( F ` A ) = C ) )
18 elex 
 |-  ( C e. V -> C e. _V )
19 17 18 impel 
 |-  ( ( A e. D /\ C e. V ) -> ( F ` A ) = C )