Theorem elrnmptdv

Description: Elementhood in the range of a function in maps-to notation, deduction form. (Contributed by Rohan Ridenour, 3-Aug-2023)

	Ref	Expression
Hypotheses	elrnmptdv.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
	elrnmptdv.2	⊢ ( 𝜑 → 𝐶 ∈ 𝐴 )
	elrnmptdv.3	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
	elrnmptdv.4	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → 𝐷 = 𝐵 )
Assertion	elrnmptdv	⊢ ( 𝜑 → 𝐷 ∈ ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		elrnmptdv.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2		elrnmptdv.2	⊢ ( 𝜑 → 𝐶 ∈ 𝐴 )
3		elrnmptdv.3	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
4		elrnmptdv.4	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → 𝐷 = 𝐵 )
5	4 2	rspcime	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 𝐷 = 𝐵 )
6	1	elrnmpt	⊢ ( 𝐷 ∈ 𝑉 → ( 𝐷 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 𝐷 = 𝐵 ) )
7	3 6	syl	⊢ ( 𝜑 → ( 𝐷 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 𝐷 = 𝐵 ) )
8	5 7	mpbird	⊢ ( 𝜑 → 𝐷 ∈ ran 𝐹 )