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 syl5ibr 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