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

Metamath Proof Explorer

Theorem iinab

Description: Indexed intersection of a class abstraction. (Contributed by NM, 6-Dec-2011)

Ref Expression
Assertion iinab ∩ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } = { 𝑦 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 }

Proof

Step Hyp Ref Expression
1 nfcv ⊢ Ⅎ 𝑦 𝐴
2 nfab1 ⊢ Ⅎ 𝑦 { 𝑦 ∣ 𝜑 }
3 1 2 nfiin ⊢ Ⅎ 𝑦 ∩ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 }
4 nfab1 ⊢ Ⅎ 𝑦 { 𝑦 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 }
5 3 4 cleqf ⊢ ( ∩ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } = { 𝑦 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } ↔ ∀ 𝑦 ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑦 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } ) )
6 abid ⊢ ( 𝑦 ∈ { 𝑦 ∣ 𝜑 } ↔ 𝜑 )
7 6 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 𝑦 ∈ { 𝑦 ∣ 𝜑 } ↔ ∀ 𝑥 ∈ 𝐴 𝜑 )
8 eliin ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ { 𝑦 ∣ 𝜑 } ) )
9 8 elv ⊢ ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ { 𝑦 ∣ 𝜑 } )
10 abid ⊢ ( 𝑦 ∈ { 𝑦 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } ↔ ∀ 𝑥 ∈ 𝐴 𝜑 )
11 7 9 10 3bitr4i ⊢ ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑦 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } )
12 5 11 mpgbir ⊢ ∩ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } = { 𝑦 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 }