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

Metamath Proof Explorer

Theorem iotaint

Description: Equivalence between two different forms of iota . (Contributed by Mario Carneiro, 24-Dec-2016)

		Ref	Expression
	Assertion	iotaint	$⊢ \exists! x φ \to (ι x \| φ) = ⋂ \{x \| φ\}$

Step	Hyp	Ref	Expression
1		iotauni	$⊢ \exists! x φ \to (ι x \| φ) = ⋃ \{x \| φ\}$
2		uniintab	$⊢ \exists! x φ \leftrightarrow ⋃ \{x \| φ\} = ⋂ \{x \| φ\}$
3	2	biimpi	$⊢ \exists! x φ \to ⋃ \{x \| φ\} = ⋂ \{x \| φ\}$
4	1 3	eqtrd	$⊢ \exists! x φ \to (ι x \| φ) = ⋂ \{x \| φ\}$