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	⊢ ( ( 𝐹 '''' 𝐴 ) = ∅ → 𝐹 defAt 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ndfatafv2	⊢ ( ¬ 𝐹 defAt 𝐴 → ( 𝐹 '''' 𝐴 ) = 𝒫 ∪ ran 𝐹 )
2		pwne0	⊢ 𝒫 ∪ ran 𝐹 ≠ ∅
3	2	neii	⊢ ¬ 𝒫 ∪ ran 𝐹 = ∅
4		eqeq1	⊢ ( ( 𝐹 '''' 𝐴 ) = 𝒫 ∪ ran 𝐹 → ( ( 𝐹 '''' 𝐴 ) = ∅ ↔ 𝒫 ∪ ran 𝐹 = ∅ ) )
5	3 4	mtbiri	⊢ ( ( 𝐹 '''' 𝐴 ) = 𝒫 ∪ ran 𝐹 → ¬ ( 𝐹 '''' 𝐴 ) = ∅ )
6	1 5	syl	⊢ ( ¬ 𝐹 defAt 𝐴 → ¬ ( 𝐹 '''' 𝐴 ) = ∅ )
7	6	con4i	⊢ ( ( 𝐹 '''' 𝐴 ) = ∅ → 𝐹 defAt 𝐴 )