Metamath Proof Explorer


Theorem riotasbc

Description: Substitution law for descriptions. Compare iotasbc . (Contributed by NM, 23-Aug-2011) (Proof shortened by Mario Carneiro, 24-Dec-2016)

Ref Expression
Assertion riotasbc ∃!xAφ[˙ιxA|φ/x]˙φ

Proof

Step Hyp Ref Expression
1 rabssab xA|φx|φ
2 riotacl2 ∃!xAφιxA|φxA|φ
3 1 2 sselid ∃!xAφιxA|φx|φ
4 df-sbc [˙ιxA|φ/x]˙φιxA|φx|φ
5 3 4 sylibr ∃!xAφ[˙ιxA|φ/x]˙φ