Metamath Proof Explorer

Theorem afvelrnb

Description: A member of a function's range is a value of the function, analogous to fvelrnb with the additional requirement that the member must be a set. (Contributed by Alexander van der Vekens, 25-May-2017)

Ref Expression
Assertion afvelrnb ⊢ F Fn A ∧ B ∈ V → B ∈ ran ⁡ F ↔ ∃ x ∈ A F ''' x = B

Proof

Step Hyp Ref Expression
1 fnrnafv ⊢ F Fn A → ran ⁡ F = y | ∃ x ∈ A y = F ''' x
2 1 adantr ⊢ F Fn A ∧ B ∈ V → ran ⁡ F = y | ∃ x ∈ A y = F ''' x
3 2 eleq2d ⊢ F Fn A ∧ B ∈ V → B ∈ ran ⁡ F ↔ B ∈ y | ∃ x ∈ A y = F ''' x
4 eqeq1 ⊢ y = B → y = F ''' x ↔ B = F ''' x
5 eqcom ⊢ B = F ''' x ↔ F ''' x = B
6 4 5 bitrdi ⊢ y = B → y = F ''' x ↔ F ''' x = B
7 6 rexbidv ⊢ y = B → ∃ x ∈ A y = F ''' x ↔ ∃ x ∈ A F ''' x = B
8 7 elabg ⊢ B ∈ V → B ∈ y | ∃ x ∈ A y = F ''' x ↔ ∃ x ∈ A F ''' x = B
9 8 adantl ⊢ F Fn A ∧ B ∈ V → B ∈ y | ∃ x ∈ A y = F ''' x ↔ ∃ x ∈ A F ''' x = B
10 3 9 bitrd ⊢ F Fn A ∧ B ∈ V → B ∈ ran ⁡ F ↔ ∃ x ∈ A F ''' x = B