This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fnresdisj

Description: A function restricted to a class disjoint with its domain is empty. (Contributed by NM, 23-Sep-2004)

Ref Expression
Assertion fnresdisj ⊢ F Fn A → A ∩ B = ∅ ↔ F ↾ B = ∅

Proof

Step Hyp Ref Expression
1 relres ⊢ Rel ⁡ F ↾ B
2 reldm0 ⊢ Rel ⁡ F ↾ B → F ↾ B = ∅ ↔ dom ⁡ F ↾ B = ∅
3 1 2 ax-mp ⊢ F ↾ B = ∅ ↔ dom ⁡ F ↾ B = ∅
4 dmres ⊢ dom ⁡ F ↾ B = B ∩ dom ⁡ F
5 incom ⊢ B ∩ dom ⁡ F = dom ⁡ F ∩ B
6 4 5 eqtri ⊢ dom ⁡ F ↾ B = dom ⁡ F ∩ B
7 fndm ⊢ F Fn A → dom ⁡ F = A
8 7 ineq1d ⊢ F Fn A → dom ⁡ F ∩ B = A ∩ B
9 6 8 eqtrid ⊢ F Fn A → dom ⁡ F ↾ B = A ∩ B
10 9 eqeq1d ⊢ F Fn A → dom ⁡ F ↾ B = ∅ ↔ A ∩ B = ∅
11 3 10 bitr2id ⊢ F Fn A → A ∩ B = ∅ ↔ F ↾ B = ∅