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	⊢ ( ℩' 𝑥 𝜑 ) = if ( ∃! 𝑥 𝜑 , ∩ { 𝑥 ∣ 𝜑 } , V )

Proof

Step	Hyp	Ref	Expression
1		aiotaint	⊢ ( ∃! 𝑥 𝜑 → ( ℩' 𝑥 𝜑 ) = ∩ { 𝑥 ∣ 𝜑 } )
2		aiotavb	⊢ ( ¬ ∃! 𝑥 𝜑 ↔ ( ℩' 𝑥 𝜑 ) = V )
3	2	biimpi	⊢ ( ¬ ∃! 𝑥 𝜑 → ( ℩' 𝑥 𝜑 ) = V )
4		ifval	⊢ ( ( ℩' 𝑥 𝜑 ) = if ( ∃! 𝑥 𝜑 , ∩ { 𝑥 ∣ 𝜑 } , V ) ↔ ( ( ∃! 𝑥 𝜑 → ( ℩' 𝑥 𝜑 ) = ∩ { 𝑥 ∣ 𝜑 } ) ∧ ( ¬ ∃! 𝑥 𝜑 → ( ℩' 𝑥 𝜑 ) = V ) ) )
5	1 3 4	mpbir2an	⊢ ( ℩' 𝑥 𝜑 ) = if ( ∃! 𝑥 𝜑 , ∩ { 𝑥 ∣ 𝜑 } , V )