Theorem aiotaval

Description: Theorem 8.19 in Quine p. 57. This theorem is the fundamental property of (alternate) iota. (Contributed by AV, 24-Aug-2022)

	Ref	Expression
Assertion	aiotaval	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( ℩' 𝑥 𝜑 ) = 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		eusnsn	⊢ ∃! 𝑧 { 𝑧 } = { 𝑦 }
2		eqcom	⊢ ( { 𝑦 } = { 𝑧 } ↔ { 𝑧 } = { 𝑦 } )
3	2	eubii	⊢ ( ∃! 𝑧 { 𝑦 } = { 𝑧 } ↔ ∃! 𝑧 { 𝑧 } = { 𝑦 } )
4	1 3	mpbir	⊢ ∃! 𝑧 { 𝑦 } = { 𝑧 }
5		eqeq1	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } → ( { 𝑥 ∣ 𝜑 } = { 𝑧 } ↔ { 𝑦 } = { 𝑧 } ) )
6	5	eubidv	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } → ( ∃! 𝑧 { 𝑥 ∣ 𝜑 } = { 𝑧 } ↔ ∃! 𝑧 { 𝑦 } = { 𝑧 } ) )
7	4 6	mpbiri	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } → ∃! 𝑧 { 𝑥 ∣ 𝜑 } = { 𝑧 } )
8		absn	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } ↔ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) )
9		reuabaiotaiota	⊢ ( ∃! 𝑧 { 𝑥 ∣ 𝜑 } = { 𝑧 } ↔ ( ℩ 𝑥 𝜑 ) = ( ℩' 𝑥 𝜑 ) )
10		eqcom	⊢ ( ( ℩ 𝑥 𝜑 ) = ( ℩' 𝑥 𝜑 ) ↔ ( ℩' 𝑥 𝜑 ) = ( ℩ 𝑥 𝜑 ) )
11	9 10	bitri	⊢ ( ∃! 𝑧 { 𝑥 ∣ 𝜑 } = { 𝑧 } ↔ ( ℩' 𝑥 𝜑 ) = ( ℩ 𝑥 𝜑 ) )
12	7 8 11	3imtr3i	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( ℩' 𝑥 𝜑 ) = ( ℩ 𝑥 𝜑 ) )
13		iotaval	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( ℩ 𝑥 𝜑 ) = 𝑦 )
14	12 13	eqtrd	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( ℩' 𝑥 𝜑 ) = 𝑦 )