Metamath Proof Explorer

Theorem fmptapd

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

Ref Expression
Hypotheses fmptapd.0a ⊢ φ → A ∈ V
fmptapd.0b ⊢ φ → B ∈ V
fmptapd.1 ⊢ φ → R ∪ A = S
fmptapd.2 ⊢ φ ∧ x = A → C = B
Assertion fmptapd ⊢ φ → x ∈ R ⟼ C ∪ A B = x ∈ S ⟼ C

Proof

Step Hyp Ref Expression
1 fmptapd.0a ⊢ φ → A ∈ V
2 fmptapd.0b ⊢ φ → B ∈ V
3 fmptapd.1 ⊢ φ → R ∪ A = S
4 fmptapd.2 ⊢ φ ∧ 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