# Metamath Proof Explorer

## Theorem afv20defat

Description: If the alternate function value at an argument is the empty set, the function is defined at this argument. (Contributed by AV, 3-Sep-2022)

Ref Expression
Assertion afv20defat ${⊢}\left({F}\mathrm{\text{'}\text{'}\text{'}\text{'}}{A}\right)=\varnothing \to {F}\mathrm{defAt}{A}$

### Proof

Step Hyp Ref Expression
1 ndfatafv2 ${⊢}¬{F}\mathrm{defAt}{A}\to \left({F}\mathrm{\text{'}\text{'}\text{'}\text{'}}{A}\right)=𝒫\bigcup \mathrm{ran}{F}$
2 pwne0 ${⊢}𝒫\bigcup \mathrm{ran}{F}\ne \varnothing$
3 2 neii ${⊢}¬𝒫\bigcup \mathrm{ran}{F}=\varnothing$
4 eqeq1 ${⊢}\left({F}\mathrm{\text{'}\text{'}\text{'}\text{'}}{A}\right)=𝒫\bigcup \mathrm{ran}{F}\to \left(\left({F}\mathrm{\text{'}\text{'}\text{'}\text{'}}{A}\right)=\varnothing ↔𝒫\bigcup \mathrm{ran}{F}=\varnothing \right)$
5 3 4 mtbiri ${⊢}\left({F}\mathrm{\text{'}\text{'}\text{'}\text{'}}{A}\right)=𝒫\bigcup \mathrm{ran}{F}\to ¬\left({F}\mathrm{\text{'}\text{'}\text{'}\text{'}}{A}\right)=\varnothing$
6 1 5 syl ${⊢}¬{F}\mathrm{defAt}{A}\to ¬\left({F}\mathrm{\text{'}\text{'}\text{'}\text{'}}{A}\right)=\varnothing$
7 6 con4i ${⊢}\left({F}\mathrm{\text{'}\text{'}\text{'}\text{'}}{A}\right)=\varnothing \to {F}\mathrm{defAt}{A}$