Metamath Proof Explorer


Theorem riotacl2

Description: Membership law for "the unique element in A such that ph ". (Contributed by NM, 21-Aug-2011) (Revised by Mario Carneiro, 23-Dec-2016)

Ref Expression
Assertion riotacl2 ∃!xAφιxA|φxA|φ

Proof

Step Hyp Ref Expression
1 df-reu ∃!xAφ∃!xxAφ
2 iotacl ∃!xxAφιx|xAφx|xAφ
3 1 2 sylbi ∃!xAφιx|xAφx|xAφ
4 df-riota ιxA|φ=ιx|xAφ
5 df-rab xA|φ=x|xAφ
6 3 4 5 3eltr4g ∃!xAφιxA|φxA|φ