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	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∅ ∉ 𝐵 ) → ( 𝑋 ∈ 𝐴 ↔ ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∅ ∉ 𝐵 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
2	1	ffvelcdmda	⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∅ ∉ 𝐵 ) ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 )
3	2	ex	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∅ ∉ 𝐵 ) → ( 𝑋 ∈ 𝐴 → ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 ) )
4		df-nel	⊢ ( ∅ ∉ 𝐵 ↔ ¬ ∅ ∈ 𝐵 )
5		nelelne	⊢ ( ¬ ∅ ∈ 𝐵 → ( ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 → ( 𝐹 ‘ 𝑋 ) ≠ ∅ ) )
6	4 5	sylbi	⊢ ( ∅ ∉ 𝐵 → ( ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 → ( 𝐹 ‘ 𝑋 ) ≠ ∅ ) )
7		fdm	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → dom 𝐹 = 𝐴 )
8		fvfundmfvn0	⊢ ( ( 𝐹 ‘ 𝑋 ) ≠ ∅ → ( 𝑋 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝑋 } ) ) )
9		simprl	⊢ ( ( dom 𝐹 = 𝐴 ∧ ( 𝑋 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝑋 } ) ) ) → 𝑋 ∈ dom 𝐹 )
10		simpl	⊢ ( ( dom 𝐹 = 𝐴 ∧ ( 𝑋 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝑋 } ) ) ) → dom 𝐹 = 𝐴 )
11	9 10	eleqtrd	⊢ ( ( dom 𝐹 = 𝐴 ∧ ( 𝑋 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝑋 } ) ) ) → 𝑋 ∈ 𝐴 )
12	11	ex	⊢ ( dom 𝐹 = 𝐴 → ( ( 𝑋 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝑋 } ) ) → 𝑋 ∈ 𝐴 ) )
13	7 8 12	syl2im	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ( 𝐹 ‘ 𝑋 ) ≠ ∅ → 𝑋 ∈ 𝐴 ) )
14	6 13	sylan9r	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∅ ∉ 𝐵 ) → ( ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 → 𝑋 ∈ 𝐴 ) )
15	3 14	impbid	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∅ ∉ 𝐵 ) → ( 𝑋 ∈ 𝐴 ↔ ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 ) )