Description: Deduction version of fvmpt (where the definition of the mapping does not depend on the common antecedent ph ). (Contributed by Glauco Siliprandi, 23-Oct-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | fvmptd2.1 | |- F = ( x e. D |-> B ) |
|
| fvmptd2.2 | |- ( ( ph /\ x = A ) -> B = C ) |
||
| fvmptd2.3 | |- ( ph -> A e. D ) |
||
| fvmptd2.4 | |- ( ph -> C e. V ) |
||
| Assertion | fvmptd2 | |- ( ph -> ( F ` A ) = C ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fvmptd2.1 | |- F = ( x e. D |-> B ) |
|
| 2 | fvmptd2.2 | |- ( ( ph /\ x = A ) -> B = C ) |
|
| 3 | fvmptd2.3 | |- ( ph -> A e. D ) |
|
| 4 | fvmptd2.4 | |- ( ph -> C e. V ) |
|
| 5 | 1 | a1i | |- ( ph -> F = ( x e. D |-> B ) ) |
| 6 | 5 2 3 4 | fvmptd | |- ( ph -> ( F ` A ) = C ) |