Metamath Proof Explorer


Theorem fresaunres1

Description: From the union of two functions that agree on the domain overlap, either component can be recovered by restriction. (Contributed by Mario Carneiro, 16-Feb-2015)

Ref Expression
Assertion fresaunres1 F:ACG:BCFAB=GABFGA=F

Proof

Step Hyp Ref Expression
1 uncom FG=GF
2 1 reseq1i FGA=GFA
3 incom AB=BA
4 3 reseq2i FAB=FBA
5 3 reseq2i GAB=GBA
6 4 5 eqeq12i FAB=GABFBA=GBA
7 eqcom FBA=GBAGBA=FBA
8 6 7 bitri FAB=GABGBA=FBA
9 fresaunres2 G:BCF:ACGBA=FBAGFA=F
10 9 3com12 F:ACG:BCGBA=FBAGFA=F
11 8 10 syl3an3b F:ACG:BCFAB=GABGFA=F
12 2 11 eqtrid F:ACG:BCFAB=GABFGA=F