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

Metamath Proof Explorer

Theorem iinrab

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

Ref Expression
Assertion iinrab ( 𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } = { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } )

Proof

Step Hyp Ref Expression
1 r19.28zv ⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜑 ) ) )
2 1 abbidv ⊢ ( 𝐴 ≠ ∅ → { 𝑦 ∣ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) } = { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜑 ) } )
3 df-rab ⊢ { 𝑦 ∈ 𝐵 ∣ 𝜑 } = { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) }
4 3 a1i ⊢ ( 𝑥 ∈ 𝐴 → { 𝑦 ∈ 𝐵 ∣ 𝜑 } = { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) } )
5 4 iineq2i ⊢ ∩ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } = ∩ 𝑥 ∈ 𝐴 { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) }
6 iinab ⊢ ∩ 𝑥 ∈ 𝐴 { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) } = { 𝑦 ∣ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) }
7 5 6 eqtri ⊢ ∩ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } = { 𝑦 ∣ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) }
8 df-rab ⊢ { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } = { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝜑 ) }
9 2 7 8 3eqtr4g ⊢ ( 𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } = { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } )