Theorem iotauni2

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

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

Proof

Step	Hyp	Ref	Expression
1		iotaval2	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } → ( ℩ 𝑥 𝜑 ) = 𝑦 )
2		unieq	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } → ∪ { 𝑥 ∣ 𝜑 } = ∪ { 𝑦 } )
3		unisnv	⊢ ∪ { 𝑦 } = 𝑦
4	2 3	eqtr2di	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } → 𝑦 = ∪ { 𝑥 ∣ 𝜑 } )
5	1 4	eqtrd	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } → ( ℩ 𝑥 𝜑 ) = ∪ { 𝑥 ∣ 𝜑 } )
6	5	exlimiv	⊢ ( ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } → ( ℩ 𝑥 𝜑 ) = ∪ { 𝑥 ∣ 𝜑 } )