Metamath Proof Explorer
Description: Deduction version of fvmpt . (Contributed by Glauco Siliprandi, 23Oct2021)


Ref 
Expression 

Hypotheses 
fvmptd3.1 
⊢ 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) 


fvmptd3.2 
⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) 


fvmptd3.3 
⊢ ( 𝜑 → 𝐴 ∈ 𝐷 ) 


fvmptd3.4 
⊢ ( 𝜑 → 𝐶 ∈ 𝑉 ) 

Assertion 
fvmptd3 
⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = 𝐶 ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

fvmptd3.1 
⊢ 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) 
2 

fvmptd3.2 
⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) 
3 

fvmptd3.3 
⊢ ( 𝜑 → 𝐴 ∈ 𝐷 ) 
4 

fvmptd3.4 
⊢ ( 𝜑 → 𝐶 ∈ 𝑉 ) 
5 
2 1

fvmptg 
⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐹 ‘ 𝐴 ) = 𝐶 ) 
6 
3 4 5

syl2anc 
⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = 𝐶 ) 