This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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