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 ⊢ F Fn A → B ∈ ran ⁡ F ↔ ∃ x ∈ A F ⁡ x = B

Proof

Step Hyp Ref Expression
1 fnrnfv ⊢ F Fn A → ran ⁡ F = y | ∃ x ∈ A y = F ⁡ x
2 1 eleq2d ⊢ F Fn A → B ∈ ran ⁡ F ↔ B ∈ y | ∃ x ∈ A y = F ⁡ x
3 fvex ⊢ F ⁡ x ∈ V
4 eleq1 ⊢ F ⁡ x = B → F ⁡ x ∈ V ↔ B ∈ V
5 3 4 mpbii ⊢ F ⁡ x = B → B ∈ V
6 5 rexlimivw ⊢ ∃ x ∈ A F ⁡ x = B → B ∈ V
7 eqeq1 ⊢ y = B → y = F ⁡ x ↔ B = F ⁡ x
8 eqcom ⊢ B = F ⁡ x ↔ F ⁡ x = B
9 7 8 bitrdi ⊢ y = B → y = F ⁡ x ↔ F ⁡ x = B
10 9 rexbidv ⊢ y = B → ∃ x ∈ A y = F ⁡ x ↔ ∃ x ∈ A F ⁡ x = B
11 6 10 elab3 ⊢ B ∈ y | ∃ x ∈ A y = F ⁡ x ↔ ∃ x ∈ A F ⁡ x = B
12 2 11 bitrdi ⊢ F Fn A → B ∈ ran ⁡ F ↔ ∃ x ∈ A F ⁡ x = B