Theorem args

Description: Two ways to express the class of unique-valued arguments of F , which is the same as the domain of F whenever F is a function. The left-hand side of the equality is from Definition 10.2 of Quine p. 65. Quine uses the notation "arg F " for this class (for which we have no separate notation). Observe the resemblance to the alternate definition dffv4 of function value, which is based on the idea in Quine's definition. (Contributed by NM, 8-May-2005)

	Ref	Expression
Assertion	args	|- { x | E. y ( F " { x } ) = { y } } = { x | E! y x F y }

Proof

Step	Hyp	Ref	Expression
1		imasng	|- ( x e. _V -> ( F " { x } ) = { y | x F y } )
2	1	elv	|- ( F " { x } ) = { y | x F y }
3	2	eqeq1i	|- ( ( F " { x } ) = { y } <-> { y | x F y } = { y } )
4	3	exbii	|- ( E. y ( F " { x } ) = { y } <-> E. y { y | x F y } = { y } )
5		euabsn	|- ( E! y x F y <-> E. y { y | x F y } = { y } )
6	4 5	bitr4i	|- ( E. y ( F " { x } ) = { y } <-> E! y x F y )
7	6	abbii	|- { x | E. y ( F " { x } ) = { y } } = { x | E! y x F y }