Theorem sn-iotalemcor

Description: Corollary of sn-iotalem . Compare sb8iota . (Contributed by SN, 6-Nov-2024)

	Ref	Expression
Assertion	sn-iotalemcor	⊢ ( ℩ 𝑥 𝜑 ) = ( ℩ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } )

Proof

Step	Hyp	Ref	Expression
1		sn-iotalem	⊢ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = { 𝑧 ∣ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = { 𝑧 } }
2	1	unieqi	⊢ ∪ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = ∪ { 𝑧 ∣ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = { 𝑧 } }
3		df-iota	⊢ ( ℩ 𝑥 𝜑 ) = ∪ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } }
4		df-iota	⊢ ( ℩ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } ) = ∪ { 𝑧 ∣ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = { 𝑧 } }
5	2 3 4	3eqtr4i	⊢ ( ℩ 𝑥 𝜑 ) = ( ℩ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } )