Metamath Proof Explorer


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 )