Metamath Proof Explorer


Theorem fndmdifeq0

Description: The difference set of two functions is empty if and only if the functions are equal. (Contributed by Stefan O'Rear, 17-Jan-2015)

Ref Expression
Assertion fndmdifeq0 F Fn A G Fn A dom F G = F = G

Proof

Step Hyp Ref Expression
1 fndmdif F Fn A G Fn A dom F G = x A | F x G x
2 1 eqeq1d F Fn A G Fn A dom F G = x A | F x G x =
3 eqfnfv F Fn A G Fn A F = G x A F x = G x
4 rabeq0 x A | F x G x = x A ¬ F x G x
5 nne ¬ F x G x F x = G x
6 5 ralbii x A ¬ F x G x x A F x = G x
7 4 6 bitri x A | F x G x = x A F x = G x
8 3 7 syl6rbbr F Fn A G Fn A x A | F x G x = F = G
9 2 8 bitrd F Fn A G Fn A dom F G = F = G