Metamath Proof Explorer


Theorem eqfnfv2f

Description: Equality of functions is determined by their values. Special case of Exercise 4 of TakeutiZaring p. 28 (with domain equality omitted). This version of eqfnfv uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 29-Jan-2004)

Ref Expression
Hypotheses eqfnfv2f.1 _ x F
eqfnfv2f.2 _ x G
Assertion eqfnfv2f F Fn A G Fn A F = G x A F x = G x

Proof

Step Hyp Ref Expression
1 eqfnfv2f.1 _ x F
2 eqfnfv2f.2 _ x G
3 eqfnfv F Fn A G Fn A F = G z A F z = G z
4 nfcv _ x z
5 1 4 nffv _ x F z
6 2 4 nffv _ x G z
7 5 6 nfeq x F z = G z
8 nfv z F x = G x
9 fveq2 z = x F z = F x
10 fveq2 z = x G z = G x
11 9 10 eqeq12d z = x F z = G z F x = G x
12 7 8 11 cbvralw z A F z = G z x A F x = G x
13 3 12 bitrdi F Fn A G Fn A F = G x A F x = G x