Theorem riotaund

Description: Restricted iota equals the empty set when not meaningful. (Contributed by NM, 16-Jan-2012) (Revised by Mario Carneiro, 15-Oct-2016) (Revised by NM, 13-Sep-2018)

	Ref	Expression
Assertion	riotaund	|- ( -. E! x e. A ph -> ( iota_ x e. A ph ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		df-riota	|- ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )
2		df-reu	|- ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
3		iotanul	|- ( -. E! x ( x e. A /\ ph ) -> ( iota x ( x e. A /\ ph ) ) = (/) )
4	2 3	sylnbi	|- ( -. E! x e. A ph -> ( iota x ( x e. A /\ ph ) ) = (/) )
5	1 4	syl5eq	|- ( -. E! x e. A ph -> ( iota_ x e. A ph ) = (/) )