Theorem iotaval

Description: Theorem 8.19 in Quine p. 57. This theorem is the fundamental property of iota. (Contributed by Andrew Salmon, 11-Jul-2011) Remove dependency on ax-10 , ax-11 , ax-12 . (Revised by SN, 23-Nov-2024)

	Ref	Expression
Assertion	iotaval	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to \left(\iota x|\phi \right)=y$$

Proof

Step	Hyp	Ref	Expression
1		abbi	$$⊢\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		iotaval2	$$⊢\left\{x|\phi \right\}=\left\{y\right\}\to \left(\iota x|\phi \right)=y$$
5	3 4	syl	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to \left(\iota x|\phi \right)=y$$