Theorem aiotaexaiotaiota

Description: The alternate iota over a wff ph is a set iff the iota and the alternate iota over ph are equal. (Contributed by AV, 25-Aug-2022)

	Ref	Expression
Assertion	aiotaexaiotaiota	|- ( ( iota' x ph ) e. _V <-> ( iota x ph ) = ( iota' x ph ) )

Proof

Step	Hyp	Ref	Expression
1		aiotaexb	|- ( E! x ph <-> ( iota' x ph ) e. _V )
2		reuaiotaiota	|- ( E! x ph <-> ( iota x ph ) = ( iota' x ph ) )
3	1 2	bitr3i	|- ( ( iota' x ph ) e. _V <-> ( iota x ph ) = ( iota' x ph ) )