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

Proof

Step	Hyp	Ref	Expression
1		reuaiotaiota	⊢ ( ∃! 𝑥 𝜑 ↔ ( ℩ 𝑥 𝜑 ) = ( ℩' 𝑥 𝜑 ) )
2	1	biimpi	⊢ ( ∃! 𝑥 𝜑 → ( ℩ 𝑥 𝜑 ) = ( ℩' 𝑥 𝜑 ) )
3		iotaint	⊢ ( ∃! 𝑥 𝜑 → ( ℩ 𝑥 𝜑 ) = ∩ { 𝑥 ∣ 𝜑 } )
4	2 3	eqtr3d	⊢ ( ∃! 𝑥 𝜑 → ( ℩' 𝑥 𝜑 ) = ∩ { 𝑥 ∣ 𝜑 } )