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	⊢ ( 𝐴 ∈ ( 𝐹 ‘ 𝐵 ) ↔ ∃ 𝑥 ( 𝐴 ∈ 𝑥 ∧ ∀ 𝑦 ( 𝐵 𝐹 𝑦 ↔ 𝑦 = 𝑥 ) ) )