Metamath Proof Explorer

Theorem elfv

Description: Membership in a function value. (Contributed by NM, 30-Apr-2004)

Ref Expression
Assertion elfv ⊢ A ∈ F ⁡ B ↔ ∃ x A ∈ x ∧ ∀ y B F y ↔ y = x

Proof

Step Hyp Ref Expression
1 fv2 ⊢ F ⁡ B = ⋃ x | ∀ y B F y ↔ y = x
2 1 eleq2i ⊢ A ∈ F ⁡ B ↔ A ∈ ⋃ x | ∀ y B F y ↔ y = x
3 eluniab ⊢ A ∈ ⋃ x | ∀ y B F y ↔ y = x ↔ ∃ x A ∈ x ∧ ∀ y B F y ↔ y = x
4 2 3 bitri ⊢ A ∈ F ⁡ B ↔ ∃ x A ∈ x ∧ ∀ y B F y ↔ y = x