This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iotaval2

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

Ref Expression
Assertion iotaval2 ( { 𝑥 ∣ 𝜑 } = { 𝑦 } → ( ℩ 𝑥 𝜑 ) = 𝑦 )

Proof

Step Hyp Ref Expression
1 df-iota ⊢ ( ℩ 𝑥 𝜑 ) = ∪ { 𝑤 ∣ { 𝑥 ∣ 𝜑 } = { 𝑤 } }
2 eqeq1 ⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } → ( { 𝑥 ∣ 𝜑 } = { 𝑤 } ↔ { 𝑦 } = { 𝑤 } ) )
3 sneqbg ⊢ ( 𝑦 ∈ V → ( { 𝑦 } = { 𝑤 } ↔ 𝑦 = 𝑤 ) )
4 3 elv ⊢ ( { 𝑦 } = { 𝑤 } ↔ 𝑦 = 𝑤 )
5 equcom ⊢ ( 𝑦 = 𝑤 ↔ 𝑤 = 𝑦 )
6 4 5 bitri ⊢ ( { 𝑦 } = { 𝑤 } ↔ 𝑤 = 𝑦 )
7 2 6 bitrdi ⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } → ( { 𝑥 ∣ 𝜑 } = { 𝑤 } ↔ 𝑤 = 𝑦 ) )
8 7 alrimiv ⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } → ∀ 𝑤 ( { 𝑥 ∣ 𝜑 } = { 𝑤 } ↔ 𝑤 = 𝑦 ) )
9 uniabio ⊢ ( ∀ 𝑤 ( { 𝑥 ∣ 𝜑 } = { 𝑤 } ↔ 𝑤 = 𝑦 ) → ∪ { 𝑤 ∣ { 𝑥 ∣ 𝜑 } = { 𝑤 } } = 𝑦 )
10 8 9 syl ⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } → ∪ { 𝑤 ∣ { 𝑥 ∣ 𝜑 } = { 𝑤 } } = 𝑦 )
11 1 10 eqtrid ⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } → ( ℩ 𝑥 𝜑 ) = 𝑦 )