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

Metamath Proof Explorer

Theorem fnsnsplit

Description: Split a function into a single point and all the rest. (Contributed by Stefan O'Rear, 27-Feb-2015)

Ref Expression
Assertion fnsnsplit ⊢ F Fn A ∧ X ∈ A → F = F ↾ A ∖ X ∪ X F ⁡ X

Proof

Step Hyp Ref Expression
1 fnresdm ⊢ F Fn A → F ↾ A = F
2 1 adantr ⊢ F Fn A ∧ X ∈ A → F ↾ A = F
3 resundi ⊢ F ↾ A ∖ X ∪ X = F ↾ A ∖ X ∪ F ↾ X
4 difsnid ⊢ X ∈ A → A ∖ X ∪ X = A
5 4 adantl ⊢ F Fn A ∧ X ∈ A → A ∖ X ∪ X = A
6 5 reseq2d ⊢ F Fn A ∧ X ∈ A → F ↾ A ∖ X ∪ X = F ↾ A
7 fnressn ⊢ F Fn A ∧ X ∈ A → F ↾ X = X F ⁡ X
8 7 uneq2d ⊢ F Fn A ∧ X ∈ A → F ↾ A ∖ X ∪ F ↾ X = F ↾ A ∖ X ∪ X F ⁡ X
9 3 6 8 3eqtr3a ⊢ F Fn A ∧ X ∈ A → F ↾ A = F ↾ A ∖ X ∪ X F ⁡ X
10 2 9 eqtr3d ⊢ F Fn A ∧ X ∈ A → F = F ↾ A ∖ X ∪ X F ⁡ X