Metamath Proof Explorer


Theorem iotaex

Description: Theorem 8.23 in Quine p. 58. This theorem proves the existence of the iota class under our definition. (Contributed by Andrew Salmon, 11-Jul-2011) Remove dependency on ax-10 , ax-11 , ax-12 . (Revised by SN, 6-Nov-2024)

Ref Expression
Assertion iotaex ( ℩ 𝑥 𝜑 ) ∈ V

Proof

Step Hyp Ref Expression
1 iotaval2 ( { 𝑥𝜑 } = { 𝑦 } → ( ℩ 𝑥 𝜑 ) = 𝑦 )
2 vex 𝑦 ∈ V
3 1 2 eqeltrdi ( { 𝑥𝜑 } = { 𝑦 } → ( ℩ 𝑥 𝜑 ) ∈ V )
4 3 exlimiv ( ∃ 𝑦 { 𝑥𝜑 } = { 𝑦 } → ( ℩ 𝑥 𝜑 ) ∈ V )
5 iotanul2 ( ¬ ∃ 𝑦 { 𝑥𝜑 } = { 𝑦 } → ( ℩ 𝑥 𝜑 ) = ∅ )
6 0ex ∅ ∈ V
7 5 6 eqeltrdi ( ¬ ∃ 𝑦 { 𝑥𝜑 } = { 𝑦 } → ( ℩ 𝑥 𝜑 ) ∈ V )
8 4 7 pm2.61i ( ℩ 𝑥 𝜑 ) ∈ V