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

Metamath Proof Explorer

Theorem iunab

Description: The indexed union of a class abstraction. (Contributed by NM, 27-Dec-2004)

Ref Expression
Assertion iunab ∪ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 }

Proof

Step Hyp Ref Expression
1 nfcv ⊢ Ⅎ 𝑦 𝐴
2 nfab1 ⊢ Ⅎ 𝑦 { 𝑦 ∣ 𝜑 }
3 1 2 nfiun ⊢ Ⅎ 𝑦 ∪ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 }
4 nfab1 ⊢ Ⅎ 𝑦 { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 }
5 3 4 cleqf ⊢ ( ∪ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } ↔ ∀ 𝑦 ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } ) )
6 abid ⊢ ( 𝑦 ∈ { 𝑦 ∣ 𝜑 } ↔ 𝜑 )
7 6 rexbii ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ { 𝑦 ∣ 𝜑 } ↔ ∃ 𝑥 ∈ 𝐴 𝜑 )
8 eliun ⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ { 𝑦 ∣ 𝜑 } )
9 abid ⊢ ( 𝑦 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } ↔ ∃ 𝑥 ∈ 𝐴 𝜑 )
10 7 8 9 3bitr4i ⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 } )
11 5 10 mpgbir ⊢ ∪ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝜑 }