# Metamath Proof Explorer

## Theorem afv2ndefb

Description: Two ways to say that an alternate function value is not defined. (Contributed by AV, 5-Sep-2022)

Ref Expression
Assertion afv2ndefb $⊢ F '''' A = 𝒫 ⋃ ran ⁡ F ↔ F '''' A ∉ ran ⁡ F$

### Proof

Step Hyp Ref Expression
1 pwuninel $⊢ ¬ 𝒫 ⋃ ran ⁡ F ∈ ran ⁡ F$
2 df-nel $⊢ F '''' A ∉ ran ⁡ F ↔ ¬ F '''' A ∈ ran ⁡ F$
3 eleq1 $⊢ F '''' A = 𝒫 ⋃ ran ⁡ F → F '''' A ∈ ran ⁡ F ↔ 𝒫 ⋃ ran ⁡ F ∈ ran ⁡ F$
4 3 notbid $⊢ F '''' A = 𝒫 ⋃ ran ⁡ F → ¬ F '''' A ∈ ran ⁡ F ↔ ¬ 𝒫 ⋃ ran ⁡ F ∈ ran ⁡ F$
5 2 4 syl5bb $⊢ F '''' A = 𝒫 ⋃ ran ⁡ F → F '''' A ∉ ran ⁡ F ↔ ¬ 𝒫 ⋃ ran ⁡ F ∈ ran ⁡ F$
6 1 5 mpbiri $⊢ F '''' A = 𝒫 ⋃ ran ⁡ F → F '''' A ∉ ran ⁡ F$
7 funressndmafv2rn $⊢ F defAt A → F '''' A ∈ ran ⁡ F$
8 7 con3i $⊢ ¬ F '''' A ∈ ran ⁡ F → ¬ F defAt A$
9 2 8 sylbi $⊢ F '''' A ∉ ran ⁡ F → ¬ F defAt A$
10 ndfatafv2 $⊢ ¬ F defAt A → F '''' A = 𝒫 ⋃ ran ⁡ F$
11 9 10 syl $⊢ F '''' A ∉ ran ⁡ F → F '''' A = 𝒫 ⋃ ran ⁡ F$
12 6 11 impbii $⊢ F '''' A = 𝒫 ⋃ ran ⁡ F ↔ F '''' A ∉ ran ⁡ F$