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

Metamath Proof Explorer

Theorem riotaclbgBAD

Description: Closure of restricted iota. (Contributed by NM, 28-Feb-2013) (Revised by Mario Carneiro, 24-Dec-2016)

Ref Expression
Assertion riotaclbgBAD 
|- ( A e. V -> ( 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 undefnel2 
 |-  ( A e. V -> -. ( Undef ` A ) e. A )
3 iffalse 
 |-  ( -. E! x e. A ph -> if ( E! x e. A ph , ( iota x ( x e. A /\ ph ) ) , ( Undef ` { x | x e. A } ) ) = ( Undef ` { x | x e. A } ) )
4 ax-riotaBAD 
 |-  ( iota_ x e. A ph ) = if ( E! x e. A ph , ( iota x ( x e. A /\ ph ) ) , ( Undef ` { x | x e. A } ) )
5 abid1 
 |-  A = { x | x e. A }
6 5 fveq2i 
 |-  ( Undef ` A ) = ( Undef ` { x | x e. A } )
7 3 4 6 3eqtr4g 
 |-  ( -. E! x e. A ph -> ( iota_ x e. A ph ) = ( Undef ` A ) )
8 7 eleq1d 
 |-  ( -. E! x e. A ph -> ( ( iota_ x e. A ph ) e. A <-> ( Undef ` A ) e. A ) )
9 8 notbid 
 |-  ( -. E! x e. A ph -> ( -. ( iota_ x e. A ph ) e. A <-> -. ( Undef ` A ) e. A ) )
10 2 9 syl5ibrcom 
 |-  ( A e. V -> ( -. E! x e. A ph -> -. ( iota_ x e. A ph ) e. A ) )
11 10 con4d 
 |-  ( A e. V -> ( ( iota_ x e. A ph ) e. A -> E! x e. A ph ) )
12 1 11 impbid2 
 |-  ( A e. V -> ( E! x e. A ph <-> ( iota_ x e. A ph ) e. A ) )