Theorem sn-iotaval

Description: iotaval without ax-10 , ax-11 , ax-12 . (Contributed by SN, 23-Nov-2024)

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

Proof

Step	Hyp	Ref	Expression
1		abbi1sn	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to \left\{x|\phi \right\}=\left\{y\right\}$$
2		iotavallem	$$⊢\left\{x|\phi \right\}=\left\{y\right\}\to \left(\iota x|\phi \right)=y$$
3	1 2	syl	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to \left(\iota x|\phi \right)=y$$