Theorem aiotaint

Description: This is to df-aiota what iotauni is to df-iota (it uses intersection like df-aiota , similar to iotauni using union like df-iota ; we could also prove an analogous result using union here too, in the same way that we have iotaint ). (Contributed by BJ, 31-Aug-2024)

	Ref	Expression
Assertion	aiotaint	|- ( E! x ph -> ( iota' x ph ) = |^| { x | ph } )

Proof

Step	Hyp	Ref	Expression
1		reuaiotaiota	|- ( E! x ph <-> ( iota x ph ) = ( iota' x ph ) )
2	1	biimpi	|- ( E! x ph -> ( iota x ph ) = ( iota' x ph ) )
3		iotaint	|- ( E! x ph -> ( iota x ph ) = |^| { x | ph } )
4	2 3	eqtr3d	|- ( E! x ph -> ( iota' x ph ) = |^| { x | ph } )