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

Metamath Proof Explorer

Theorem fvelrnb

Description: A member of a function's range is a value of the function. (Contributed by NM, 31-Oct-1995)

Ref Expression
Assertion fvelrnb ( 𝐹 Fn 𝐴 → ( 𝐵 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fnrnfv ⊢ ( 𝐹 Fn 𝐴 → ran 𝐹 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) } )
2 1 eleq2d ⊢ ( 𝐹 Fn 𝐴 → ( 𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) } ) )
3 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
4 eleq1 ⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝐵 → ( ( 𝐹 ‘ 𝑥 ) ∈ V ↔ 𝐵 ∈ V ) )
5 3 4 mpbii ⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝐵 → 𝐵 ∈ V )
6 5 rexlimivw ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝐵 → 𝐵 ∈ V )
7 eqeq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ 𝐵 = ( 𝐹 ‘ 𝑥 ) ) )
8 eqcom ⊢ ( 𝐵 = ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) = 𝐵 )
9 7 8 bitrdi ⊢ ( 𝑦 = 𝐵 → ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) = 𝐵 ) )
10 9 rexbidv ⊢ ( 𝑦 = 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝐵 ) )
11 6 10 elab3 ⊢ ( 𝐵 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑥 ) } ↔ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝐵 )
12 2 11 bitrdi ⊢ ( 𝐹 Fn 𝐴 → ( 𝐵 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝐵 ) )