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 ( 𝑥𝐴 { 𝑦𝐵𝜑 } ∩ 𝐵 ) = { 𝑦𝐵 ∣ ∀ 𝑥𝐴 𝜑 }