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 rabeq0 ⊢ x ∈ A | F ⁡ x ≠ G ⁡ x = ∅ ↔ ∀ x ∈ A ¬ F ⁡ x ≠ G ⁡ x
4 nne ⊢ ¬ F ⁡ x ≠ G ⁡ x ↔ F ⁡ x = G ⁡ x
5 4 ralbii ⊢ ∀ x ∈ A ¬ F ⁡ x ≠ G ⁡ x ↔ ∀ x ∈ A F ⁡ x = G ⁡ x
6 3 5 bitri ⊢ x ∈ A | F ⁡ x ≠ G ⁡ x = ∅ ↔ ∀ x ∈ A F ⁡ x = G ⁡ x
7 eqfnfv ⊢ F Fn A ∧ G Fn A → F = G ↔ ∀ x ∈ A F ⁡ x = G ⁡ x
8 6 7 bitr4id ⊢ 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