Theorem iotan0aiotaex

Description: If the iota over a wff ph is not empty, the alternate iota over ph is a set. (Contributed by AV, 25-Aug-2022)

	Ref	Expression
Assertion	iotan0aiotaex	⊢ ( ( ℩ 𝑥 𝜑 ) ≠ ∅ → ( ℩' 𝑥 𝜑 ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		iotanul	⊢ ( ¬ ∃! 𝑥 𝜑 → ( ℩ 𝑥 𝜑 ) = ∅ )
2	1	necon1ai	⊢ ( ( ℩ 𝑥 𝜑 ) ≠ ∅ → ∃! 𝑥 𝜑 )
3		aiotaexb	⊢ ( ∃! 𝑥 𝜑 ↔ ( ℩' 𝑥 𝜑 ) ∈ V )
4	2 3	sylib	⊢ ( ( ℩ 𝑥 𝜑 ) ≠ ∅ → ( ℩' 𝑥 𝜑 ) ∈ V )