iotajust

Description: Soundness justification theorem for df-iota . (Contributed by Andrew Salmon, 29-Jun-2011)

		Ref	Expression
	Assertion	iotajust	$⊢ ⋃ \{y \| \{x \| φ\} = \{y\}\} = ⋃ \{z \| \{x \| φ\} = \{z\}\}$

Step	Hyp	Ref	Expression
1		sneq	$⊢ y = w \to \{y\} = \{w\}$
2	1	eqeq2d	$⊢ y = w \to (\{x \| φ\} = \{y\} \leftrightarrow \{x \| φ\} = \{w\})$
3	2	cbvabv	$⊢ \{y \| \{x \| φ\} = \{y\}\} = \{w \| \{x \| φ\} = \{w\}\}$
4		sneq	$⊢ w = z \to \{w\} = \{z\}$
5	4	eqeq2d	$⊢ w = z \to (\{x \| φ\} = \{w\} \leftrightarrow \{x \| φ\} = \{z\})$
6	5	cbvabv	$⊢ \{w \| \{x \| φ\} = \{w\}\} = \{z \| \{x \| φ\} = \{z\}\}$
7	3 6	eqtri	$⊢ \{y \| \{x \| φ\} = \{y\}\} = \{z \| \{x \| φ\} = \{z\}\}$
8	7	unieqi	$⊢ ⋃ \{y \| \{x \| φ\} = \{y\}\} = ⋃ \{z \| \{x \| φ\} = \{z\}\}$

Metamath Proof Explorer