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

Metamath Proof Explorer

Theorem elrnmptg

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

Ref Expression
Hypothesis rnmpt.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
Assertion elrnmptg ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ( 𝐶 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 rnmpt.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2 1 rnmpt ⊢ ran 𝐹 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 }
3 2 eleq2i ⊢ ( 𝐶 ∈ ran 𝐹 ↔ 𝐶 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )
4 r19.29 ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 ) → ∃ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝑉 ∧ 𝐶 = 𝐵 ) )
5 eleq1 ⊢ ( 𝐶 = 𝐵 → ( 𝐶 ∈ 𝑉 ↔ 𝐵 ∈ 𝑉 ) )
6 5 biimparc ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 = 𝐵 ) → 𝐶 ∈ 𝑉 )
7 6 elexd ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 = 𝐵 ) → 𝐶 ∈ V )
8 7 rexlimivw ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝑉 ∧ 𝐶 = 𝐵 ) → 𝐶 ∈ V )
9 4 8 syl ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 ) → 𝐶 ∈ V )
10 9 ex ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ( ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 → 𝐶 ∈ V ) )
11 eqeq1 ⊢ ( 𝑦 = 𝐶 → ( 𝑦 = 𝐵 ↔ 𝐶 = 𝐵 ) )
12 11 rexbidv ⊢ ( 𝑦 = 𝐶 → ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 ) )
13 12 elab3g ⊢ ( ( ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 → 𝐶 ∈ V ) → ( 𝐶 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ↔ ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 ) )
14 10 13 syl ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ( 𝐶 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ↔ ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 ) )
15 3 14 bitrid ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ( 𝐶 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 ) )