This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fmptapd

Description: Append an additional value to a function. (Contributed by Thierry Arnoux, 3-Jan-2017) (Revised by AV, 10-Aug-2024)

Ref Expression
Hypotheses fmptapd.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
fmptapd.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
fmptapd.s ⊢ ( 𝜑 → ( 𝑅 ∪ { 𝐴 } ) = 𝑆 )
fmptapd.c ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐶 = 𝐵 )
Assertion fmptapd ( 𝜑 → ( ( 𝑥 ∈ 𝑅 ↦ 𝐶 ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) = ( 𝑥 ∈ 𝑆 ↦ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 fmptapd.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 fmptapd.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3 fmptapd.s ⊢ ( 𝜑 → ( 𝑅 ∪ { 𝐴 } ) = 𝑆 )
4 fmptapd.c ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝐶 = 𝐵 )
5 4 1 2 fmptsnd ⊢ ( 𝜑 → { ⟨ 𝐴 , 𝐵 ⟩ } = ( 𝑥 ∈ { 𝐴 } ↦ 𝐶 ) )
6 5 uneq2d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑅 ↦ 𝐶 ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) = ( ( 𝑥 ∈ 𝑅 ↦ 𝐶 ) ∪ ( 𝑥 ∈ { 𝐴 } ↦ 𝐶 ) ) )
7 mptun ⊢ ( 𝑥 ∈ ( 𝑅 ∪ { 𝐴 } ) ↦ 𝐶 ) = ( ( 𝑥 ∈ 𝑅 ↦ 𝐶 ) ∪ ( 𝑥 ∈ { 𝐴 } ↦ 𝐶 ) )
8 7 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑅 ∪ { 𝐴 } ) ↦ 𝐶 ) = ( ( 𝑥 ∈ 𝑅 ↦ 𝐶 ) ∪ ( 𝑥 ∈ { 𝐴 } ↦ 𝐶 ) ) )
9 3 mpteq1d ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑅 ∪ { 𝐴 } ) ↦ 𝐶 ) = ( 𝑥 ∈ 𝑆 ↦ 𝐶 ) )
10 6 8 9 3eqtr2d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑅 ↦ 𝐶 ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) = ( 𝑥 ∈ 𝑆 ↦ 𝐶 ) )