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

Metamath Proof Explorer

Theorem iotaequ

Description: Theorem *14.2 in WhiteheadRussell p. 189. (Contributed by Andrew Salmon, 11-Jul-2011)

		Ref	Expression
	Assertion	iotaequ	$⊢ (ι x \| x = y) = y$

Step	Hyp	Ref	Expression
1		iotaval	$⊢ \forall x (x = y \leftrightarrow x = y) \to (ι x \| x = y) = y$
2		biid	$⊢ x = y \leftrightarrow x = y$
3	1 2	mpg	$⊢ (ι x \| x = y) = y$