Theorem sn-iotauni

Description: Version of iotauni using df-iota instead of dfiota2 . (Contributed by SN, 6-Nov-2024)

	Ref	Expression
Assertion	sn-iotauni	⊢ ( ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } → ( ℩ 𝑥 𝜑 ) = ∪ { 𝑥 ∣ 𝜑 } )

Proof

Step	Hyp	Ref	Expression
1		sn-iotaval	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } → ( ℩ 𝑥 𝜑 ) = 𝑦 )
2		unieq	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } → ∪ { 𝑥 ∣ 𝜑 } = ∪ { 𝑦 } )
3		vex	⊢ 𝑦 ∈ V
4	3	unisn	⊢ ∪ { 𝑦 } = 𝑦
5	2 4	eqtr2di	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } → 𝑦 = ∪ { 𝑥 ∣ 𝜑 } )
6	1 5	eqtrd	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } → ( ℩ 𝑥 𝜑 ) = ∪ { 𝑥 ∣ 𝜑 } )
7	6	exlimiv	⊢ ( ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } → ( ℩ 𝑥 𝜑 ) = ∪ { 𝑥 ∣ 𝜑 } )