This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐹 )