Theorem elrnmpt1d

Description: Elementhood in an image set. Deducion version of elrnmpt1 . (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	elrnmpt1d.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
	elrnmpt1d.2	⊢ ( 𝜑 → 𝑥 ∈ 𝐴 )
	elrnmpt1d.3	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
Assertion	elrnmpt1d	⊢ ( 𝜑 → 𝐵 ∈ ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		elrnmpt1d.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2		elrnmpt1d.2	⊢ ( 𝜑 → 𝑥 ∈ 𝐴 )
3		elrnmpt1d.3	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
4	1	elrnmpt1	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉 ) → 𝐵 ∈ ran 𝐹 )
5	2 3 4	syl2anc	⊢ ( 𝜑 → 𝐵 ∈ ran 𝐹 )