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)

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

Proof

Step	Hyp	Ref	Expression
1		dfiota2	⊢ ( ℩ 𝑥 𝜑 ) = ∪ { 𝑧 ∣ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) }
2		sbeqalb	⊢ ( 𝑦 ∈ V → ( ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ) → 𝑦 = 𝑧 ) )
3	2	elv	⊢ ( ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ) → 𝑦 = 𝑧 )
4	3	ex	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) → 𝑦 = 𝑧 ) )
5		equequ2	⊢ ( 𝑦 = 𝑧 → ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑧 ) )
6	5	bibi2d	⊢ ( 𝑦 = 𝑧 → ( ( 𝜑 ↔ 𝑥 = 𝑦 ) ↔ ( 𝜑 ↔ 𝑥 = 𝑧 ) ) )
7	6	biimpd	⊢ ( 𝑦 = 𝑧 → ( ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( 𝜑 ↔ 𝑥 = 𝑧 ) ) )
8	7	alimdv	⊢ ( 𝑦 = 𝑧 → ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ) )
9	8	com12	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( 𝑦 = 𝑧 → ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ) )
10	4 9	impbid	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ↔ 𝑦 = 𝑧 ) )
11		equcom	⊢ ( 𝑦 = 𝑧 ↔ 𝑧 = 𝑦 )
12	10 11	bitrdi	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ↔ 𝑧 = 𝑦 ) )
13	12	alrimiv	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ∀ 𝑧 ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ↔ 𝑧 = 𝑦 ) )
14		uniabio	⊢ ( ∀ 𝑧 ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ↔ 𝑧 = 𝑦 ) → ∪ { 𝑧 ∣ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) } = 𝑦 )
15	13 14	syl	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ∪ { 𝑧 ∣ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) } = 𝑦 )
16	1 15	eqtrid	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( ℩ 𝑥 𝜑 ) = 𝑦 )