Metamath Proof Explorer


Theorem fvreseq0

Description: Equality of restricted functions is determined by their values (for functions with different domains). (Contributed by AV, 6-Jan-2019)

Ref Expression
Assertion fvreseq0 F Fn A G Fn C B A B C F B = G B x B F x = G x

Proof

Step Hyp Ref Expression
1 fnssres F Fn A B A F B Fn B
2 fnssres G Fn C B C G B Fn B
3 eqfnfv F B Fn B G B Fn B F B = G B x B F B x = G B x
4 fvres x B F B x = F x
5 fvres x B G B x = G x
6 4 5 eqeq12d x B F B x = G B x F x = G x
7 6 ralbiia x B F B x = G B x x B F x = G x
8 3 7 bitrdi F B Fn B G B Fn B F B = G B x B F x = G x
9 1 2 8 syl2an F Fn A B A G Fn C B C F B = G B x B F x = G x
10 9 an4s F Fn A G Fn C B A B C F B = G B x B F x = G x