Theorem viin

Description: Indexed intersection with a universal index class. When A doesn't depend on x , this evaluates to A by 19.3 and abid2 . When A = x , this evaluates to (/) by intiin and intv . (Contributed by NM, 11-Sep-2008)

	Ref	Expression
Assertion	viin	⊢ ∩ 𝑥 ∈ V 𝐴 = { 𝑦 ∣ ∀ 𝑥 𝑦 ∈ 𝐴 }

Proof

Step	Hyp	Ref	Expression
1		df-iin	⊢ ∩ 𝑥 ∈ V 𝐴 = { 𝑦 ∣ ∀ 𝑥 ∈ V 𝑦 ∈ 𝐴 }
2		ralv	⊢ ( ∀ 𝑥 ∈ V 𝑦 ∈ 𝐴 ↔ ∀ 𝑥 𝑦 ∈ 𝐴 )
3	2	abbii	⊢ { 𝑦 ∣ ∀ 𝑥 ∈ V 𝑦 ∈ 𝐴 } = { 𝑦 ∣ ∀ 𝑥 𝑦 ∈ 𝐴 }
4	1 3	eqtri	⊢ ∩ 𝑥 ∈ V 𝐴 = { 𝑦 ∣ ∀ 𝑥 𝑦 ∈ 𝐴 }