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

Metamath Proof Explorer

Theorem iotauni2

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

		Ref	Expression
	Assertion	iotauni2	$⊢ \exists y \{x \| φ\} = \{y\} \to (ι x \| φ) = ⋃ \{x \| φ\}$

Step	Hyp	Ref	Expression
1		iotaval2	$⊢ \{x \| φ\} = \{y\} \to (ι x \| φ) = y$
2		unieq	$⊢ \{x \| φ\} = \{y\} \to ⋃ \{x \| φ\} = ⋃ \{y\}$
3		unisnv	$⊢ ⋃ \{y\} = y$
4	2 3	eqtr2di	$⊢ \{x \| φ\} = \{y\} \to y = ⋃ \{x \| φ\}$
5	1 4	eqtrd	$⊢ \{x \| φ\} = \{y\} \to (ι x \| φ) = ⋃ \{x \| φ\}$
6	5	exlimiv	$⊢ \exists y \{x \| φ\} = \{y\} \to (ι x \| φ) = ⋃ \{x \| φ\}$