Theorem elrnmpt2d

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

	Ref	Expression
Hypotheses	elrnmpt2d.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
	elrnmpt2d.2	⊢ ( 𝜑 → 𝐶 ∈ ran 𝐹 )
Assertion	elrnmpt2d	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		elrnmpt2d.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2		elrnmpt2d.2	⊢ ( 𝜑 → 𝐶 ∈ ran 𝐹 )
3	1	elrnmpt	⊢ ( 𝐶 ∈ ran 𝐹 → ( 𝐶 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 ) )
4	3	ibi	⊢ ( 𝐶 ∈ ran 𝐹 → ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 )
5	2 4	syl	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 )