Theorem ndmfvrcl

Description: Reverse closure law for function with the empty set not in its domain. (Contributed by NM, 26-Apr-1996)

	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	⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑆 → 𝐴 ∈ 𝑆 )