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

Metamath Proof Explorer

Theorem elrnmpti

Description: Membership in the range of a function. (Contributed by NM, 30-Aug-2004) (Revised by Mario Carneiro, 31-Aug-2015)

Ref Expression
Hypotheses rnmpt.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
elrnmpti.2 ⊢ 𝐵 ∈ V
Assertion elrnmpti ( 𝐶 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 )

Proof

Step Hyp Ref Expression
1 rnmpt.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2 elrnmpti.2 ⊢ 𝐵 ∈ V
3 2 rgenw ⊢ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V
4 1 elrnmptg ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V → ( 𝐶 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 ) )
5 3 4 ax-mp ⊢ ( 𝐶 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 )