This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )