Metamath Proof Explorer


Theorem iotassuniOLD

Description: Obsolete version of iotassuni as of 23-Dec-2024. (Contributed by Mario Carneiro, 24-Dec-2016) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion iotassuniOLD ( ℩ 𝑥 𝜑 ) ⊆ { 𝑥𝜑 }

Proof

Step Hyp Ref Expression
1 iotauni ( ∃! 𝑥 𝜑 → ( ℩ 𝑥 𝜑 ) = { 𝑥𝜑 } )
2 eqimss ( ( ℩ 𝑥 𝜑 ) = { 𝑥𝜑 } → ( ℩ 𝑥 𝜑 ) ⊆ { 𝑥𝜑 } )
3 1 2 syl ( ∃! 𝑥 𝜑 → ( ℩ 𝑥 𝜑 ) ⊆ { 𝑥𝜑 } )
4 iotanul ( ¬ ∃! 𝑥 𝜑 → ( ℩ 𝑥 𝜑 ) = ∅ )
5 0ss ∅ ⊆ { 𝑥𝜑 }
6 4 5 eqsstrdi ( ¬ ∃! 𝑥 𝜑 → ( ℩ 𝑥 𝜑 ) ⊆ { 𝑥𝜑 } )
7 3 6 pm2.61i ( ℩ 𝑥 𝜑 ) ⊆ { 𝑥𝜑 }