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