Theorem elrnmptd

Description: The range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	elrnmptd.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
	elrnmptd.x	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 )
	elrnmptd.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
Assertion	elrnmptd	⊢ ( 𝜑 → 𝐶 ∈ ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		elrnmptd.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2		elrnmptd.x	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 )
3		elrnmptd.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
4	1	elrnmpt	⊢ ( 𝐶 ∈ 𝑉 → ( 𝐶 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 ) )
5	3 4	syl	⊢ ( 𝜑 → ( 𝐶 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 ) )
6	2 5	mpbird	⊢ ( 𝜑 → 𝐶 ∈ ran 𝐹 )