Theorem riotaclb

Description: Bidirectional closure of restricted iota when domain is not empty. (Contributed by NM, 28-Feb-2013) (Revised by Mario Carneiro, 24-Dec-2016) (Revised by NM, 13-Sep-2018)

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

Proof

Step	Hyp	Ref	Expression
1		riotacl	|- ( E! x e. A ph -> ( iota_ x e. A ph ) e. A )
2		riotaund	|- ( -. E! x e. A ph -> ( iota_ x e. A ph ) = (/) )
3	2	eleq1d	|- ( -. E! x e. A ph -> ( ( iota_ x e. A ph ) e. A <-> (/) e. A ) )
4	3	notbid	|- ( -. E! x e. A ph -> ( -. ( iota_ x e. A ph ) e. A <-> -. (/) e. A ) )
5	4	biimprcd	|- ( -. (/) e. A -> ( -. E! x e. A ph -> -. ( iota_ x e. A ph ) e. A ) )
6	5	con4d	|- ( -. (/) e. A -> ( ( iota_ x e. A ph ) e. A -> E! x e. A ph ) )
7	1 6	impbid2	|- ( -. (/) e. A -> ( E! x e. A ph <-> ( iota_ x e. A ph ) e. A ) )