Description: Version of iotauni using df-iota instead of dfiota2 . (Contributed by SN, 6-Nov-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | iotauni2 | ⊢ ( ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } → ( ℩ 𝑥 𝜑 ) = ∪ { 𝑥 ∣ 𝜑 } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iotaval2 | ⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } → ( ℩ 𝑥 𝜑 ) = 𝑦 ) | |
2 | unieq | ⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } → ∪ { 𝑥 ∣ 𝜑 } = ∪ { 𝑦 } ) | |
3 | unisnv | ⊢ ∪ { 𝑦 } = 𝑦 | |
4 | 2 3 | eqtr2di | ⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } → 𝑦 = ∪ { 𝑥 ∣ 𝜑 } ) |
5 | 1 4 | eqtrd | ⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } → ( ℩ 𝑥 𝜑 ) = ∪ { 𝑥 ∣ 𝜑 } ) |
6 | 5 | exlimiv | ⊢ ( ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } → ( ℩ 𝑥 𝜑 ) = ∪ { 𝑥 ∣ 𝜑 } ) |