Metamath Proof Explorer

Theorem feldmfvelcdm

Description: A class is an element of the domain iff it's function value is an element of the codomain of a function. (Contributed by AV, 22-Apr-2025)

Ref Expression
Assertion feldmfvelcdm ⊢ F : A ⟶ B ∧ ∅ ∉ B → X ∈ A ↔ F ⁡ X ∈ B

Proof

Step Hyp Ref Expression
1 simpl ⊢ F : A ⟶ B ∧ ∅ ∉ B → F : A ⟶ B
2 1 ffvelcdmda ⊢ F : A ⟶ B ∧ ∅ ∉ B ∧ X ∈ A → F ⁡ X ∈ B
3 2 ex ⊢ F : A ⟶ B ∧ ∅ ∉ B → X ∈ A → F ⁡ X ∈ B
4 df-nel ⊢ ∅ ∉ B ↔ ¬ ∅ ∈ B
5 nelelne ⊢ ¬ ∅ ∈ B → F ⁡ X ∈ B → F ⁡ X ≠ ∅
6 4 5 sylbi ⊢ ∅ ∉ B → F ⁡ X ∈ B → F ⁡ X ≠ ∅
7 fdm ⊢ F : A ⟶ B → dom ⁡ F = A
8 fvfundmfvn0 ⊢ F ⁡ X ≠ ∅ → X ∈ dom ⁡ F ∧ Fun ⁡ F ↾ X
9 simprl ⊢ dom ⁡ F = A ∧ X ∈ dom ⁡ F ∧ Fun ⁡ F ↾ X → X ∈ dom ⁡ F
10 simpl ⊢ dom ⁡ F = A ∧ X ∈ dom ⁡ F ∧ Fun ⁡ F ↾ X → dom ⁡ F = A
11 9 10 eleqtrd ⊢ dom ⁡ F = A ∧ X ∈ dom ⁡ F ∧ Fun ⁡ F ↾ X → X ∈ A
12 11 ex ⊢ dom ⁡ F = A → X ∈ dom ⁡ F ∧ Fun ⁡ F ↾ X → X ∈ A
13 7 8 12 syl2im ⊢ F : A ⟶ B → F ⁡ X ≠ ∅ → X ∈ A
14 6 13 sylan9r ⊢ F : A ⟶ B ∧ ∅ ∉ B → F ⁡ X ∈ B → X ∈ A
15 3 14 impbid ⊢ F : A ⟶ B ∧ ∅ ∉ B → X ∈ A ↔ F ⁡ X ∈ B