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		abid	⊢ ( 𝑦 ∈ { 𝑦 ∣ 𝜑 } ↔ 𝜑 )
6	5	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑦 ∈ { 𝑦 ∣ 𝜑 } ↔ ∀ 𝑥 ∈ 𝐴 𝜑 )
7		eliin	⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ { 𝑦 ∣ 𝜑 } ) )
8	7	elv	⊢ ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ { 𝑦 ∣ 𝜑 } )
9		abid	⊢ ( 𝑦 ∈ { 𝑦 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } ↔ ∀ 𝑥 ∈ 𝐴 𝜑 )
10	6 8 9	3bitr4i	⊢ ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑦 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 } )
11	3 4 10	eqri	⊢ ∩ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } = { 𝑦 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 }