Theorem uniabio

Description: Part of Theorem 8.17 in Quine p. 56. This theorem serves as a lemma for the fundamental property of iota. (Contributed by Andrew Salmon, 11-Jul-2011)

	Ref	Expression
Assertion	uniabio	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ∪ { 𝑥 ∣ 𝜑 } = 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		abbi1	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝑥 = 𝑦 } )
2		df-sn	⊢ { 𝑦 } = { 𝑥 ∣ 𝑥 = 𝑦 }
3	1 2	eqtr4di	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → { 𝑥 ∣ 𝜑 } = { 𝑦 } )
4	3	unieqd	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ∪ { 𝑥 ∣ 𝜑 } = ∪ { 𝑦 } )
5		vex	⊢ 𝑦 ∈ V
6	5	unisn	⊢ ∪ { 𝑦 } = 𝑦
7	4 6	eqtrdi	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ∪ { 𝑥 ∣ 𝜑 } = 𝑦 )