Metamath Proof Explorer


Theorem iotauni2

Description: Version of iotauni using df-iota instead of dfiota2 . (Contributed by SN, 6-Nov-2024)

Ref Expression
Assertion iotauni2 ( ∃ 𝑦 { 𝑥𝜑 } = { 𝑦 } → ( ℩ 𝑥 𝜑 ) = { 𝑥𝜑 } )

Proof

Step Hyp Ref Expression
1 iotaval2 ( { 𝑥𝜑 } = { 𝑦 } → ( ℩ 𝑥 𝜑 ) = 𝑦 )
2 unieq ( { 𝑥𝜑 } = { 𝑦 } → { 𝑥𝜑 } = { 𝑦 } )
3 unisnv { 𝑦 } = 𝑦
4 2 3 eqtr2di ( { 𝑥𝜑 } = { 𝑦 } → 𝑦 = { 𝑥𝜑 } )
5 1 4 eqtrd ( { 𝑥𝜑 } = { 𝑦 } → ( ℩ 𝑥 𝜑 ) = { 𝑥𝜑 } )
6 5 exlimiv ( ∃ 𝑦 { 𝑥𝜑 } = { 𝑦 } → ( ℩ 𝑥 𝜑 ) = { 𝑥𝜑 } )