# 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}\to \left({A}\cap {B}=\varnothing ↔{{F}↾}_{{B}}=\varnothing \right)$

### Proof

Step Hyp Ref Expression
1 relres ${⊢}\mathrm{Rel}\left({{F}↾}_{{B}}\right)$
2 reldm0 ${⊢}\mathrm{Rel}\left({{F}↾}_{{B}}\right)\to \left({{F}↾}_{{B}}=\varnothing ↔\mathrm{dom}\left({{F}↾}_{{B}}\right)=\varnothing \right)$
3 1 2 ax-mp ${⊢}{{F}↾}_{{B}}=\varnothing ↔\mathrm{dom}\left({{F}↾}_{{B}}\right)=\varnothing$
4 dmres ${⊢}\mathrm{dom}\left({{F}↾}_{{B}}\right)={B}\cap \mathrm{dom}{F}$
5 incom ${⊢}{B}\cap \mathrm{dom}{F}=\mathrm{dom}{F}\cap {B}$
6 4 5 eqtri ${⊢}\mathrm{dom}\left({{F}↾}_{{B}}\right)=\mathrm{dom}{F}\cap {B}$
7 fndm ${⊢}{F}Fn{A}\to \mathrm{dom}{F}={A}$
8 7 ineq1d ${⊢}{F}Fn{A}\to \mathrm{dom}{F}\cap {B}={A}\cap {B}$
9 6 8 syl5eq ${⊢}{F}Fn{A}\to \mathrm{dom}\left({{F}↾}_{{B}}\right)={A}\cap {B}$
10 9 eqeq1d ${⊢}{F}Fn{A}\to \left(\mathrm{dom}\left({{F}↾}_{{B}}\right)=\varnothing ↔{A}\cap {B}=\varnothing \right)$
11 3 10 syl5rbb ${⊢}{F}Fn{A}\to \left({A}\cap {B}=\varnothing ↔{{F}↾}_{{B}}=\varnothing \right)$