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

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 )