Theorem uniabio

Description: Part of Theorem 8.17 in Quine p. 56. This theorem serves as a lemma for the fundamental property of iota. (Contributed by Andrew Salmon, 11-Jul-2011)

	Ref	Expression
Assertion	uniabio	|- ( A. x ( ph <-> x = y ) -> U. { x | ph } = y )

Proof

Step	Hyp	Ref	Expression
1		abbi1	|- ( A. x ( ph <-> x = y ) -> { x | ph } = { x | x = y } )
2		df-sn	|- { y } = { x | x = y }
3	1 2	eqtr4di	|- ( A. x ( ph <-> x = y ) -> { x | ph } = { y } )
4	3	unieqd	|- ( A. x ( ph <-> x = y ) -> U. { x | ph } = U. { y } )
5		vex	|- y e. _V
6	5	unisn	|- U. { y } = y
7	4 6	eqtrdi	|- ( A. x ( ph <-> x = y ) -> U. { x | ph } = y )