Theorem afv2fv0xorb

Description: If a set is in the range of a function, the function's value at an argument is the empty set if and only if the alternate function value at this argument is either the empty set or undefined. (Contributed by AV, 11-Sep-2022)

	Ref	Expression
Assertion	afv2fv0xorb	⊢ ( ∅ ∈ ran 𝐹 → ( ( 𝐹 ‘ 𝐴 ) = ∅ ↔ ( ( 𝐹 '''' 𝐴 ) = ∅ ⊻ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		afv2fv0b	⊢ ( ( 𝐹 ‘ 𝐴 ) = ∅ ↔ ( ( 𝐹 '''' 𝐴 ) = ∅ ∨ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) )
2		afv2orxorb	⊢ ( ∅ ∈ ran 𝐹 → ( ( ( 𝐹 '''' 𝐴 ) = ∅ ∨ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) ↔ ( ( 𝐹 '''' 𝐴 ) = ∅ ⊻ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) ) )
3	1 2	syl5bb	⊢ ( ∅ ∈ ran 𝐹 → ( ( 𝐹 ‘ 𝐴 ) = ∅ ↔ ( ( 𝐹 '''' 𝐴 ) = ∅ ⊻ ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 ) ) )