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	|- ( ( F '''' A ) = (/) -> F defAt A )

Proof

Step	Hyp	Ref	Expression
1		ndfatafv2	|- ( -. F defAt A -> ( F '''' A ) = ~P U. ran F )
2		pwne0	|- ~P U. ran F =/= (/)
3	2	neii	|- -. ~P U. ran F = (/)
4		eqeq1	|- ( ( F '''' A ) = ~P U. ran F -> ( ( F '''' A ) = (/) <-> ~P U. ran F = (/) ) )
5	3 4	mtbiri	|- ( ( F '''' A ) = ~P U. ran F -> -. ( F '''' A ) = (/) )
6	1 5	syl	|- ( -. F defAt A -> -. ( F '''' A ) = (/) )
7	6	con4i	|- ( ( F '''' A ) = (/) -> F defAt A )