Theorem rr-elrnmpt3d

Description: Elementhood in an image set. (Contributed by Rohan Ridenour, 11-Aug-2023)

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

Proof

Step	Hyp	Ref	Expression
1		rr-elrnmpt3d.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2		rr-elrnmpt3d.2	⊢ ( 𝜑 → 𝐶 ∈ 𝐴 )
3		rr-elrnmpt3d.3	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
4		rr-elrnmpt3d.4	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → 𝐵 = 𝐷 )
5	4	eqcomd	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐶 ) → 𝐷 = 𝐵 )
6	1 2 3 5	elrnmptdv	⊢ ( 𝜑 → 𝐷 ∈ ran 𝐹 )