This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⁡ F = S
ndmfvrcl.2 ⊢ ¬ ∅ ∈ R
Assertion ndmfvrcl ⊢ F ⁡ A ∈ R → A ∈ S

Proof

Step Hyp Ref Expression
1 ndmfvrcl.1 ⊢ dom ⁡ F = S
2 ndmfvrcl.2 ⊢ ¬ ∅ ∈ R
3 ndmfv ⊢ ¬ A ∈ dom ⁡ F → F ⁡ A = ∅
4 3 eleq1d ⊢ ¬ A ∈ dom ⁡ F → F ⁡ A ∈ R ↔ ∅ ∈ R
5 2 4 mtbiri ⊢ ¬ A ∈ dom ⁡ F → ¬ F ⁡ A ∈ R
6 5 con4i ⊢ F ⁡ A ∈ R → A ∈ dom ⁡ F
7 6 1 eleqtrdi ⊢ F ⁡ A ∈ R → A ∈ S