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 ⊢ φ → A ∈ V
fmptapd.b ⊢ φ → B ∈ W
fmptapd.s ⊢ φ → R ∪ A = S
fmptapd.c ⊢ φ ∧ x = A → C = B
Assertion fmptapd ⊢ φ → x ∈ R ⟼ C ∪ A B = x ∈ S ⟼ C

Proof

Step Hyp Ref Expression
1 fmptapd.a ⊢ φ → A ∈ V
2 fmptapd.b ⊢ φ → B ∈ W
3 fmptapd.s ⊢ φ → R ∪ A = S
4 fmptapd.c ⊢ φ ∧ x = A → C = B
5 4 1 2 fmptsnd ⊢ φ → A B = x ∈ A ⟼ C
6 5 uneq2d ⊢ φ → x ∈ R ⟼ C ∪ A B = x ∈ R ⟼ C ∪ x ∈ A ⟼ C
7 mptun ⊢ x ∈ R ∪ A ⟼ C = x ∈ R ⟼ C ∪ x ∈ A ⟼ C
8 7 a1i ⊢ φ → x ∈ R ∪ A ⟼ C = x ∈ R ⟼ C ∪ x ∈ A ⟼ C
9 3 mpteq1d ⊢ φ → x ∈ R ∪ A ⟼ C = x ∈ S ⟼ C
10 6 8 9 3eqtr2d ⊢ φ → x ∈ R ⟼ C ∪ A B = x ∈ S ⟼ C