Theorem iinab

Description: Indexed intersection of a class builder. (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	⊢ ∩ 𝑥 ∈ 𝐴 { 𝑦 ∣ 𝜑 } = { 𝑦 ∣ ∀ 𝑥 ∈ 𝐴 𝜑 }