Description: Deduction version of fvmpt . (Contributed by Scott Fenton, 18-Feb-2013) (Revised by Mario Carneiro, 31-Aug-2015) (Proof shortened by AV, 29-Mar-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | fvmptd.1 | |- ( ph -> F = ( x e. D |-> B ) ) |
|
| fvmptd.2 | |- ( ( ph /\ x = A ) -> B = C ) |
||
| fvmptd.3 | |- ( ph -> A e. D ) |
||
| fvmptd.4 | |- ( ph -> C e. V ) |
||
| Assertion | fvmptd | |- ( ph -> ( F ` A ) = C ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fvmptd.1 | |- ( ph -> F = ( x e. D |-> B ) ) |
|
| 2 | fvmptd.2 | |- ( ( ph /\ x = A ) -> B = C ) |
|
| 3 | fvmptd.3 | |- ( ph -> A e. D ) |
|
| 4 | fvmptd.4 | |- ( ph -> C e. V ) |
|
| 5 | nfv | |- F/ x ph |
|
| 6 | nfcv | |- F/_ x A |
|
| 7 | nfcv | |- F/_ x C |
|
| 8 | 1 2 3 4 5 6 7 | fvmptdf | |- ( ph -> ( F ` A ) = C ) |