Theorem ndmfvrcl

Description: Reverse closure law for function with the empty set not in its domain (if R = S ). (Contributed by NM, 26-Apr-1996) The class containing the function value does not have to be the domain. (Revised by Zhi Wang, 10-Nov-2025)

	Ref	Expression
Hypotheses	ndmfvrcl.1	⊢ dom 𝐹 = 𝑆
	ndmfvrcl.2	⊢ ¬ ∅ ∈ 𝑅
Assertion	ndmfvrcl	⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑅 → 𝐴 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		ndmfvrcl.1	⊢ dom 𝐹 = 𝑆
2		ndmfvrcl.2	⊢ ¬ ∅ ∈ 𝑅
3		ndmfv	⊢ ( ¬ 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∅ )
4	3	eleq1d	⊢ ( ¬ 𝐴 ∈ dom 𝐹 → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑅 ↔ ∅ ∈ 𝑅 ) )
5	2 4	mtbiri	⊢ ( ¬ 𝐴 ∈ dom 𝐹 → ¬ ( 𝐹 ‘ 𝐴 ) ∈ 𝑅 )
6	5	con4i	⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑅 → 𝐴 ∈ dom 𝐹 )
7	6 1	eleqtrdi	⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑅 → 𝐴 ∈ 𝑆 )