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

Metamath Proof Explorer

Theorem riinrab

Description: Relative intersection of a relative abstraction. (Contributed by Stefan O'Rear, 3-Apr-2015)

Ref Expression
Assertion riinrab ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝐴 ∣ 𝜑 } ) = { 𝑦 ∈ 𝐴 ∣ ∀ 𝑥 ∈ 𝑋 𝜑 }

Proof

Step Hyp Ref Expression
1 riin0 ⊢ ( 𝑋 = ∅ → ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝐴 ∣ 𝜑 } ) = 𝐴 )
2 rzal ⊢ ( 𝑋 = ∅ → ∀ 𝑥 ∈ 𝑋 𝜑 )
3 2 ralrimivw ⊢ ( 𝑋 = ∅ → ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝑋 𝜑 )
4 rabid2 ⊢ ( 𝐴 = { 𝑦 ∈ 𝐴 ∣ ∀ 𝑥 ∈ 𝑋 𝜑 } ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝑋 𝜑 )
5 3 4 sylibr ⊢ ( 𝑋 = ∅ → 𝐴 = { 𝑦 ∈ 𝐴 ∣ ∀ 𝑥 ∈ 𝑋 𝜑 } )
6 1 5 eqtrd ⊢ ( 𝑋 = ∅ → ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝐴 ∣ 𝜑 } ) = { 𝑦 ∈ 𝐴 ∣ ∀ 𝑥 ∈ 𝑋 𝜑 } )
7 ssrab2 ⊢ { 𝑦 ∈ 𝐴 ∣ 𝜑 } ⊆ 𝐴
8 7 rgenw ⊢ ∀ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝐴 ∣ 𝜑 } ⊆ 𝐴
9 riinn0 ⊢ ( ( ∀ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝐴 ∣ 𝜑 } ⊆ 𝐴 ∧ 𝑋 ≠ ∅ ) → ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝐴 ∣ 𝜑 } ) = ∩ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝐴 ∣ 𝜑 } )
10 8 9 mpan ⊢ ( 𝑋 ≠ ∅ → ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝐴 ∣ 𝜑 } ) = ∩ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝐴 ∣ 𝜑 } )
11 iinrab ⊢ ( 𝑋 ≠ ∅ → ∩ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝐴 ∣ 𝜑 } = { 𝑦 ∈ 𝐴 ∣ ∀ 𝑥 ∈ 𝑋 𝜑 } )
12 10 11 eqtrd ⊢ ( 𝑋 ≠ ∅ → ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝐴 ∣ 𝜑 } ) = { 𝑦 ∈ 𝐴 ∣ ∀ 𝑥 ∈ 𝑋 𝜑 } )
13 6 12 pm2.61ine ⊢ ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝐴 ∣ 𝜑 } ) = { 𝑦 ∈ 𝐴 ∣ ∀ 𝑥 ∈ 𝑋 𝜑 }