Theorem elfv

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

	Ref	Expression
Assertion	elfv	$$⊢A\in F\left(B\right)\leftrightarrow \exists x\left(A\in x\wedge \forall y\left(BFy\leftrightarrow y=x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		fv2	$$⊢F\left(B\right)=\bigcup \left\{x|\forall y\left(BFy\leftrightarrow y=x\right)\right\}$$
2	1	eleq2i	$$⊢A\in F\left(B\right)\leftrightarrow A\in \bigcup \left\{x|\forall y\left(BFy\leftrightarrow y=x\right)\right\}$$
3		eluniab	$$⊢A\in \bigcup \left\{x|\forall y\left(BFy\leftrightarrow y=x\right)\right\}\leftrightarrow \exists x\left(A\in x\wedge \forall y\left(BFy\leftrightarrow y=x\right)\right)$$
4	2 3	bitri	$$⊢A\in F\left(B\right)\leftrightarrow \exists x\left(A\in x\wedge \forall y\left(BFy\leftrightarrow y=x\right)\right)$$