Theorem opabiotadm

Description: Define a function whose value is "the unique y such that ph ( x , y ) ". (Contributed by NM, 16-Nov-2013)

	Ref	Expression
Hypothesis	opabiota.1	|- F = { <. x , y >. | { y | ph } = { y } }
Assertion	opabiotadm	|- dom F = { x | E! y ph }

Proof

Step	Hyp	Ref	Expression
1		opabiota.1	|- F = { <. x , y >. | { y | ph } = { y } }
2		dmopab	|- dom { <. x , y >. | { y | ph } = { y } } = { x | E. y { y | ph } = { y } }
3	1	dmeqi	|- dom F = dom { <. x , y >. | { y | ph } = { y } }
4		euabsn	|- ( E! y ph <-> E. y { y | ph } = { y } )
5	4	abbii	|- { x | E! y ph } = { x | E. y { y | ph } = { y } }
6	2 3 5	3eqtr4i	|- dom F = { x | E! y ph }