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

Metamath Proof Explorer

Theorem riotauni

Description: Restricted iota in terms of class union. (Contributed by NM, 11-Oct-2011)

Ref Expression
Assertion riotauni 
|- ( E! x e. A ph -> ( iota_ x e. A ph ) = U. { x e. A | ph } )

Proof

Step Hyp Ref Expression
1 df-reu 
 |-  ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
2 iotauni 
 |-  ( E! x ( x e. A /\ ph ) -> ( iota x ( x e. A /\ ph ) ) = U. { x | ( x e. A /\ ph ) } )
3 1 2 sylbi 
 |-  ( E! x e. A ph -> ( iota x ( x e. A /\ ph ) ) = U. { x | ( x e. A /\ ph ) } )
4 df-riota 
 |-  ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )
5 df-rab 
 |-  { x e. A | ph } = { x | ( x e. A /\ ph ) }
6 5 unieqi 
 |-  U. { x e. A | ph } = U. { x | ( x e. A /\ ph ) }
7 3 4 6 3eqtr4g 
 |-  ( E! x e. A ph -> ( iota_ x e. A ph ) = U. { x e. A | ph } )