This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( ℩ 𝑥 𝜑 ) = 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		abbi	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝑥 = 𝑦 } )
2		df-sn	⊢ { 𝑦 } = { 𝑥 ∣ 𝑥 = 𝑦 }
3	1 2	eqtr4di	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → { 𝑥 ∣ 𝜑 } = { 𝑦 } )
4		iotaval2	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } → ( ℩ 𝑥 𝜑 ) = 𝑦 )
5	3 4	syl	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( ℩ 𝑥 𝜑 ) = 𝑦 )