Description: Alternate deduction version of fvmpt , suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017) (Proof shortened by AV, 19-Jan-2022)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | fvmptd2f.1 | |- ( ph -> A e. D ) |
|
| fvmptd2f.2 | |- ( ( ph /\ x = A ) -> B e. V ) |
||
| fvmptd2f.3 | |- ( ( ph /\ x = A ) -> ( ( F ` A ) = B -> ps ) ) |
||
| fvmptd2f.4 | |- F/_ x F |
||
| fvmptd2f.5 | |- F/ x ps |
||
| Assertion | fvmptd2f | |- ( ph -> ( F = ( x e. D |-> B ) -> ps ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fvmptd2f.1 | |- ( ph -> A e. D ) |
|
| 2 | fvmptd2f.2 | |- ( ( ph /\ x = A ) -> B e. V ) |
|
| 3 | fvmptd2f.3 | |- ( ( ph /\ x = A ) -> ( ( F ` A ) = B -> ps ) ) |
|
| 4 | fvmptd2f.4 | |- F/_ x F |
|
| 5 | fvmptd2f.5 | |- F/ x ps |
|
| 6 | nfv | |- F/ x ph |
|
| 7 | 1 2 3 4 5 6 | fvmptd3f | |- ( ph -> ( F = ( x e. D |-> B ) -> ps ) ) |