Metamath Proof Explorer


Theorem eqfnov2

Description: Two operators with the same domain are equal iff their values at each point in the domain are equal. (Contributed by Jeff Madsen, 7-Jun-2010)

Ref Expression
Assertion eqfnov2 F Fn A × B G Fn A × B F = G x A y B x F y = x G y

Proof

Step Hyp Ref Expression
1 eqfnov F Fn A × B G Fn A × B F = G A × B = A × B x A y B x F y = x G y
2 simpr A × B = A × B x A y B x F y = x G y x A y B x F y = x G y
3 eqidd x A y B x F y = x G y A × B = A × B
4 3 ancri x A y B x F y = x G y A × B = A × B x A y B x F y = x G y
5 2 4 impbii A × B = A × B x A y B x F y = x G y x A y B x F y = x G y
6 1 5 bitrdi F Fn A × B G Fn A × B F = G x A y B x F y = x G y