Metamath Proof Explorer


Theorem elfv

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

Ref Expression
Assertion elfv ( 𝐴 ∈ ( 𝐹𝐵 ) ↔ ∃ 𝑥 ( 𝐴𝑥 ∧ ∀ 𝑦 ( 𝐵 𝐹 𝑦𝑦 = 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 fv2 ( 𝐹𝐵 ) = { 𝑥 ∣ ∀ 𝑦 ( 𝐵 𝐹 𝑦𝑦 = 𝑥 ) }
2 1 eleq2i ( 𝐴 ∈ ( 𝐹𝐵 ) ↔ 𝐴 { 𝑥 ∣ ∀ 𝑦 ( 𝐵 𝐹 𝑦𝑦 = 𝑥 ) } )
3 eluniab ( 𝐴 { 𝑥 ∣ ∀ 𝑦 ( 𝐵 𝐹 𝑦𝑦 = 𝑥 ) } ↔ ∃ 𝑥 ( 𝐴𝑥 ∧ ∀ 𝑦 ( 𝐵 𝐹 𝑦𝑦 = 𝑥 ) ) )
4 2 3 bitri ( 𝐴 ∈ ( 𝐹𝐵 ) ↔ ∃ 𝑥 ( 𝐴𝑥 ∧ ∀ 𝑦 ( 𝐵 𝐹 𝑦𝑦 = 𝑥 ) ) )