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

Metamath Proof Explorer

Theorem iinrab2

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

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

Proof

Step Hyp Ref Expression
1 iineq1 ⊢ ( 𝐴 = ∅ → ∩ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } = ∩ 𝑥 ∈ ∅ { 𝑦 ∈ 𝐵 ∣ 𝜑 } )
2 0iin ⊢ ∩ 𝑥 ∈ ∅ { 𝑦 ∈ 𝐵 ∣ 𝜑 } = V
3 1 2 eqtrdi ⊢ ( 𝐴 = ∅ → ∩ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } = V )
4 3 ineq1d ⊢ ( 𝐴 = ∅ → ( ∩ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∩ 𝐵 ) = ( V ∩ 𝐵 ) )
5 incom ⊢ ( V ∩ 𝐵 ) = ( 𝐵 ∩ V )
6 inv1 ⊢ ( 𝐵 ∩ V ) = 𝐵
7 5 6 eqtri ⊢ ( V ∩ 𝐵 ) = 𝐵
8 4 7 eqtrdi ⊢ ( 𝐴 = ∅ → ( ∩ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∩ 𝐵 ) = 𝐵 )
9 rzal ⊢ ( 𝐴 = ∅ → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 )
10 rabid2 ⊢ ( 𝐵 = { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 𝜑 )
11 ralcom ⊢ ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 )
12 10 11 bitr2i ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ↔ 𝐵 = { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } )
13 9 12 sylib ⊢ ( 𝐴 = ∅ → 𝐵 = { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } )
14 8 13 eqtrd ⊢ ( 𝐴 = ∅ → ( ∩ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∩ 𝐵 ) = { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } )
15 iinrab ⊢ ( 𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } = { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } )
16 15 ineq1d ⊢ ( 𝐴 ≠ ∅ → ( ∩ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∩ 𝐵 ) = ( { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } ∩ 𝐵 ) )
17 ssrab2 ⊢ { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } ⊆ 𝐵
18 dfss ⊢ ( { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } ⊆ 𝐵 ↔ { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } = ( { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } ∩ 𝐵 ) )
19 17 18 mpbi ⊢ { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } = ( { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } ∩ 𝐵 )
20 16 19 eqtr4di ⊢ ( 𝐴 ≠ ∅ → ( ∩ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∩ 𝐵 ) = { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } )
21 14 20 pm2.61ine ⊢ ( ∩ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∩ 𝐵 ) = { 𝑦 ∈ 𝐵 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 }