This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sn-iotalemcor

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

		Ref	Expression
	Assertion	sn-iotalemcor	$⊢ (ι x \| φ) = (ι y \| \{x \| φ\} = \{y\})$

Step	Hyp	Ref	Expression
1		sn-iotalem	$⊢ \{y \| \{x \| φ\} = \{y\}\} = \{z \| \{y \| \{x \| φ\} = \{y\}\} = \{z\}\}$
2	1	unieqi	$⊢ ⋃ \{y \| \{x \| φ\} = \{y\}\} = ⋃ \{z \| \{y \| \{x \| φ\} = \{y\}\} = \{z\}\}$
3		df-iota	$⊢ (ι x \| φ) = ⋃ \{y \| \{x \| φ\} = \{y\}\}$
4		df-iota	$⊢ (ι y \| \{x \| φ\} = \{y\}) = ⋃ \{z \| \{y \| \{x \| φ\} = \{y\}\} = \{z\}\}$
5	2 3 4	3eqtr4i	$⊢ (ι x \| φ) = (ι y \| \{x \| φ\} = \{y\})$