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 𝐹 ↔ ∃ 𝑥𝐴 ( 𝐹𝑥 ) = 𝐵 ) )