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	|- ( E! x e. A ph -> [. ( iota_ x e. A ph ) / x ]. ph )

Proof

Step	Hyp	Ref	Expression
1		rabssab	|- { x e. A | ph } C_ { x | ph }
2		riotacl2	|- ( E! x e. A ph -> ( iota_ x e. A ph ) e. { x e. A | ph } )
3	1 2	sseldi	|- ( E! x e. A ph -> ( iota_ x e. A ph ) e. { x | ph } )
4		df-sbc	|- ( [. ( iota_ x e. A ph ) / x ]. ph <-> ( iota_ x e. A ph ) e. { x | ph } )
5	3 4	sylibr	|- ( E! x e. A ph -> [. ( iota_ x e. A ph ) / x ]. ph )