Theorem aiotavb

Description: The alternate iota over a wff ph is the universe iff there is no unique value x satisfying ph . (Contributed by AV, 25-Aug-2022)

	Ref	Expression
Assertion	aiotavb	⊢ ( ¬ ∃! 𝑥 𝜑 ↔ ( ℩' 𝑥 𝜑 ) = V )

Proof

Step	Hyp	Ref	Expression
1		intnex	⊢ ( ¬ ∩ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } ∈ V ↔ ∩ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = V )
2		df-aiota	⊢ ( ℩' 𝑥 𝜑 ) = ∩ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } }
3	2	eleq1i	⊢ ( ( ℩' 𝑥 𝜑 ) ∈ V ↔ ∩ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } ∈ V )
4	3	notbii	⊢ ( ¬ ( ℩' 𝑥 𝜑 ) ∈ V ↔ ¬ ∩ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } ∈ V )
5	2	eqeq1i	⊢ ( ( ℩' 𝑥 𝜑 ) = V ↔ ∩ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = V )
6	1 4 5	3bitr4i	⊢ ( ¬ ( ℩' 𝑥 𝜑 ) ∈ V ↔ ( ℩' 𝑥 𝜑 ) = V )
7		aiotaexb	⊢ ( ∃! 𝑥 𝜑 ↔ ( ℩' 𝑥 𝜑 ) ∈ V )
8	6 7	xchnxbir	⊢ ( ¬ ∃! 𝑥 𝜑 ↔ ( ℩' 𝑥 𝜑 ) = V )