Theorem fv2

Description: Alternate definition of function value. Definition 10.11 of Quine p. 68. (Contributed by NM, 30-Apr-2004) (Proof shortened by Andrew Salmon, 17-Sep-2011) (Revised by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Assertion	fv2	$$⊢F\left(A\right)=\bigcup \left\{x|\forall y\left(AFy\leftrightarrow y=x\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-fv	$$⊢F\left(A\right)=\left(\iota y|AFy\right)$$
2		dfiota2	$$⊢\left(\iota y|AFy\right)=\bigcup \left\{x|\forall y\left(AFy\leftrightarrow y=x\right)\right\}$$
3	1 2	eqtri	$$⊢F\left(A\right)=\bigcup \left\{x|\forall y\left(AFy\leftrightarrow y=x\right)\right\}$$