Metamath Proof Explorer

Theorem eqfnun

Description: Two functions on A u. B are equal if and only if they have equal restrictions to both A and B . (Contributed by Jeff Madsen, 19-Jun-2011)

Ref Expression
Assertion eqfnun ⊢ F Fn A ∪ B ∧ G Fn A ∪ B → F = G ↔ F ↾ A = G ↾ A ∧ F ↾ B = G ↾ B

Proof

Step Hyp Ref Expression
1 reseq1 ⊢ F = G → F ↾ A = G ↾ A
2 reseq1 ⊢ F = G → F ↾ B = G ↾ B
3 1 2 jca ⊢ F = G → F ↾ A = G ↾ A ∧ F ↾ B = G ↾ B
4 elun ⊢ x ∈ A ∪ B ↔ x ∈ A ∨ x ∈ B
5 fveq1 ⊢ F ↾ A = G ↾ A → F ↾ A ⁡ x = G ↾ A ⁡ x
6 fvres ⊢ x ∈ A → F ↾ A ⁡ x = F ⁡ x
7 5 6 sylan9req ⊢ F ↾ A = G ↾ A ∧ x ∈ A → G ↾ A ⁡ x = F ⁡ x
8 fvres ⊢ x ∈ A → G ↾ A ⁡ x = G ⁡ x
9 8 adantl ⊢ F ↾ A = G ↾ A ∧ x ∈ A → G ↾ A ⁡ x = G ⁡ x
10 7 9 eqtr3d ⊢ F ↾ A = G ↾ A ∧ x ∈ A → F ⁡ x = G ⁡ x
11 10 adantlr ⊢ F ↾ A = G ↾ A ∧ F ↾ B = G ↾ B ∧ x ∈ A → F ⁡ x = G ⁡ x
12 fveq1 ⊢ F ↾ B = G ↾ B → F ↾ B ⁡ x = G ↾ B ⁡ x
13 fvres ⊢ x ∈ B → F ↾ B ⁡ x = F ⁡ x
14 12 13 sylan9req ⊢ F ↾ B = G ↾ B ∧ x ∈ B → G ↾ B ⁡ x = F ⁡ x
15 fvres ⊢ x ∈ B → G ↾ B ⁡ x = G ⁡ x
16 15 adantl ⊢ F ↾ B = G ↾ B ∧ x ∈ B → G ↾ B ⁡ x = G ⁡ x
17 14 16 eqtr3d ⊢ F ↾ B = G ↾ B ∧ x ∈ B → F ⁡ x = G ⁡ x
18 17 adantll ⊢ F ↾ A = G ↾ A ∧ F ↾ B = G ↾ B ∧ x ∈ B → F ⁡ x = G ⁡ x
19 11 18 jaodan ⊢ F ↾ A = G ↾ A ∧ F ↾ B = G ↾ B ∧ x ∈ A ∨ x ∈ B → F ⁡ x = G ⁡ x
20 4 19 sylan2b ⊢ F ↾ A = G ↾ A ∧ F ↾ B = G ↾ B ∧ x ∈ A ∪ B → F ⁡ x = G ⁡ x
21 20 ralrimiva ⊢ F ↾ A = G ↾ A ∧ F ↾ B = G ↾ B → ∀ x ∈ A ∪ B F ⁡ x = G ⁡ x
22 eqfnfv ⊢ F Fn A ∪ B ∧ G Fn A ∪ B → F = G ↔ ∀ x ∈ A ∪ B F ⁡ x = G ⁡ x
23 21 22 imbitrrid ⊢ F Fn A ∪ B ∧ G Fn A ∪ B → F ↾ A = G ↾ A ∧ F ↾ B = G ↾ B → F = G
24 3 23 impbid2 ⊢ F Fn A ∪ B ∧ G Fn A ∪ B → F = G ↔ F ↾ A = G ↾ A ∧ F ↾ B = G ↾ B