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	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to \bigcup \left\{x|\phi \right\}=y$$

Proof

Step	Hyp	Ref	Expression
1		abbi1	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to \left\{x|\phi \right\}=\left\{x|x=y\right\}$$
2		df-sn	$$⊢\left\{y\right\}=\left\{x|x=y\right\}$$
3	1 2	eqtr4di	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to \left\{x|\phi \right\}=\left\{y\right\}$$
4	3	unieqd	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to \bigcup \left\{x|\phi \right\}=\bigcup \left\{y\right\}$$
5		vex	$$⊢y\in \mathrm{V}$$
6	5	unisn	$$⊢\bigcup \left\{y\right\}=y$$
7	4 6	eqtrdi	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to \bigcup \left\{x|\phi \right\}=y$$