Theorem dfaiota3

Description: Alternate definition of iota' : this is to df-aiota what dfiota4 is to df-iota . operation using the if operator. It is simpler than df-aiota and uses no dummy variables, so it would be the preferred definition if iota' becomes the description binder used in set.mm. (Contributed by BJ, 31-Aug-2024)

	Ref	Expression
Assertion	dfaiota3	|- ( iota' x ph ) = if ( E! x ph , |^| { x | ph } , _V )

Proof

Step	Hyp	Ref	Expression
1		aiotaint	|- ( E! x ph -> ( iota' x ph ) = |^| { x | ph } )
2		aiotavb	|- ( -. E! x ph <-> ( iota' x ph ) = _V )
3	2	biimpi	|- ( -. E! x ph -> ( iota' x ph ) = _V )
4		ifval	|- ( ( iota' x ph ) = if ( E! x ph , |^| { x | ph } , _V ) <-> ( ( E! x ph -> ( iota' x ph ) = |^| { x | ph } ) /\ ( -. E! x ph -> ( iota' x ph ) = _V ) ) )
5	1 3 4	mpbir2an	|- ( iota' x ph ) = if ( E! x ph , |^| { x | ph } , _V )