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 ⊢FFnA∪B∧GFnA∪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∪BF⁡x=G⁡x
22 eqfnfv ⊢FFnA∪B∧GFnA∪B→F=G↔∀x∈A∪BF⁡x=G⁡x
23 21 22 imbitrrid ⊢FFnA∪B∧GFnA∪B→F↾A=G↾A∧F↾B=G↾B→F=G
24 3 23 impbid2 ⊢FFnA∪B∧GFnA∪B→F=G↔F↾A=G↾A∧F↾B=G↾B