This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - add the Axiom of Power Sets Functions fvmptd
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 ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) )
fvmptd.2 ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐵 = 𝐶 )
fvmptd.3 ⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
fvmptd.4 ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
Assertion
fvmptd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = 𝐶 )
Proof
Step
Hyp
Ref
Expression
1
fvmptd.1 ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) )
2
fvmptd.2 ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐵 = 𝐶 )
3
fvmptd.3 ⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
4
fvmptd.4 ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
5
nfv ⊢ Ⅎ 𝑥 𝜑
6
nfcv ⊢ Ⅎ 𝑥 𝐴
7
nfcv ⊢ Ⅎ 𝑥 𝐶
8
1 2 3 4 5 6 7
fvmptdf ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = 𝐶 )