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

Metamath Proof Explorer

Theorem fmptap

Description: Append an additional value to a function. (Contributed by NM, 6-Jun-2006) (Revised by Mario Carneiro, 31-Aug-2015)

Ref Expression
Hypotheses fmptap.0a ⊢ 𝐴 ∈ V
fmptap.0b ⊢ 𝐵 ∈ V
fmptap.1 ⊢ ( 𝑅 ∪ { 𝐴 } ) = 𝑆
fmptap.2 ⊢ ( 𝑥 = 𝐴 → 𝐶 = 𝐵 )
Assertion fmptap ( ( 𝑥 ∈ 𝑅 ↦ 𝐶 ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) = ( 𝑥 ∈ 𝑆 ↦ 𝐶 )

Proof

Step Hyp Ref Expression
1 fmptap.0a ⊢ 𝐴 ∈ V
2 fmptap.0b ⊢ 𝐵 ∈ V
3 fmptap.1 ⊢ ( 𝑅 ∪ { 𝐴 } ) = 𝑆
4 fmptap.2 ⊢ ( 𝑥 = 𝐴 → 𝐶 = 𝐵 )
5 fmptsn ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → { ⟨ 𝐴 , 𝐵 ⟩ } = ( 𝑥 ∈ { 𝐴 } ↦ 𝐵 ) )
6 1 2 5 mp2an ⊢ { ⟨ 𝐴 , 𝐵 ⟩ } = ( 𝑥 ∈ { 𝐴 } ↦ 𝐵 )
7 elsni ⊢ ( 𝑥 ∈ { 𝐴 } → 𝑥 = 𝐴 )
8 7 4 syl ⊢ ( 𝑥 ∈ { 𝐴 } → 𝐶 = 𝐵 )
9 8 mpteq2ia ⊢ ( 𝑥 ∈ { 𝐴 } ↦ 𝐶 ) = ( 𝑥 ∈ { 𝐴 } ↦ 𝐵 )
10 6 9 eqtr4i ⊢ { ⟨ 𝐴 , 𝐵 ⟩ } = ( 𝑥 ∈ { 𝐴 } ↦ 𝐶 )
11 10 uneq2i ⊢ ( ( 𝑥 ∈ 𝑅 ↦ 𝐶 ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) = ( ( 𝑥 ∈ 𝑅 ↦ 𝐶 ) ∪ ( 𝑥 ∈ { 𝐴 } ↦ 𝐶 ) )
12 mptun ⊢ ( 𝑥 ∈ ( 𝑅 ∪ { 𝐴 } ) ↦ 𝐶 ) = ( ( 𝑥 ∈ 𝑅 ↦ 𝐶 ) ∪ ( 𝑥 ∈ { 𝐴 } ↦ 𝐶 ) )
13 3 mpteq1i ⊢ ( 𝑥 ∈ ( 𝑅 ∪ { 𝐴 } ) ↦ 𝐶 ) = ( 𝑥 ∈ 𝑆 ↦ 𝐶 )
14 11 12 13 3eqtr2i ⊢ ( ( 𝑥 ∈ 𝑅 ↦ 𝐶 ) ∪ { ⟨ 𝐴 , 𝐵 ⟩ } ) = ( 𝑥 ∈ 𝑆 ↦ 𝐶 )