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

Proof

Step Hyp Ref Expression
1 iotaval x x = y x = y ι x | x = y = y
2 biid x = y x = y
3 1 2 mpg ι x | x = y = y