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 ⊢ A ∈ V
fmptap.0b ⊢ B ∈ V
fmptap.1 ⊢ R ∪ A = S
fmptap.2 ⊢ x = A → C = B
Assertion fmptap ⊢ x ∈ R ⟼ C ∪ A B = x ∈ S ⟼ C

Proof

Step Hyp Ref Expression
1 fmptap.0a ⊢ A ∈ V
2 fmptap.0b ⊢ B ∈ V
3 fmptap.1 ⊢ R ∪ A = S
4 fmptap.2 ⊢ x = A → C = B
5 fmptsn ⊢ A ∈ V ∧ B ∈ V → A B = x ∈ A ⟼ B
6 1 2 5 mp2an ⊢ A B = x ∈ A ⟼ B
7 elsni ⊢ x ∈ A → x = A
8 7 4 syl ⊢ x ∈ A → C = B
9 8 mpteq2ia ⊢ x ∈ A ⟼ C = x ∈ A ⟼ B
10 6 9 eqtr4i ⊢ A B = x ∈ A ⟼ C
11 10 uneq2i ⊢ x ∈ R ⟼ C ∪ A B = x ∈ R ⟼ C ∪ x ∈ A ⟼ C
12 mptun ⊢ x ∈ R ∪ A ⟼ C = x ∈ R ⟼ C ∪ x ∈ A ⟼ C
13 3 mpteq1i ⊢ x ∈ R ∪ A ⟼ C = x ∈ S ⟼ C
14 11 12 13 3eqtr2i ⊢ x ∈ R ⟼ C ∪ A B = x ∈ S ⟼ C