Description: Deduction version of fvmpt (where the substitution hypothesis does not have the antecedent ph ). (Contributed by SN, 26-Jul-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | fvmptd4.1 | |- ( x = A -> B = C ) |
|
fvmptd4.2 | |- ( ph -> F = ( x e. D |-> B ) ) |
||
fvmptd4.3 | |- ( ph -> A e. D ) |
||
fvmptd4.4 | |- ( ph -> C e. V ) |
||
Assertion | fvmptd4 | |- ( ph -> ( F ` A ) = C ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fvmptd4.1 | |- ( x = A -> B = C ) |
|
2 | fvmptd4.2 | |- ( ph -> F = ( x e. D |-> B ) ) |
|
3 | fvmptd4.3 | |- ( ph -> A e. D ) |
|
4 | fvmptd4.4 | |- ( ph -> C e. V ) |
|
5 | 1 | adantl | |- ( ( ph /\ x = A ) -> B = C ) |
6 | 2 5 3 4 | fvmptd | |- ( ph -> ( F ` A ) = C ) |