Metamath Proof Explorer

Theorem dfiota4

Description: The iota operation using the if operator. (Contributed by Scott Fenton, 6-Oct-2017) (Proof shortened by JJ, 28-Oct-2021)

Ref Expression
Assertion dfiota4 
|- ( iota x ph ) = if ( E! x ph , U. { x | ph } , (/) )

Proof

Step Hyp Ref Expression
1 iotauni 
 |-  ( E! x ph -> ( iota x ph ) = U. { x | ph } )
2 iotanul 
 |-  ( -. E! x ph -> ( iota x ph ) = (/) )
3 ifval 
 |-  ( ( iota x ph ) = if ( E! x ph , U. { x | ph } , (/) ) <-> ( ( E! x ph -> ( iota x ph ) = U. { x | ph } ) /\ ( -. E! x ph -> ( iota x ph ) = (/) ) ) )
4 1 2 3 mpbir2an 
 |-  ( iota x ph ) = if ( E! x ph , U. { x | ph } , (/) )