Theorem intiin

Description: Class intersection in terms of indexed intersection. Definition in Stoll p. 44. (Contributed by NM, 28-Jun-1998)

	Ref	Expression
Assertion	intiin	⊢ ∩ 𝐴 = ∩ 𝑥 ∈ 𝐴 𝑥

Proof

Step	Hyp	Ref	Expression
1		dfint2	⊢ ∩ 𝐴 = { 𝑦 ∣ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 }
2		df-iin	⊢ ∩ 𝑥 ∈ 𝐴 𝑥 = { 𝑦 ∣ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 }
3	1 2	eqtr4i	⊢ ∩ 𝐴 = ∩ 𝑥 ∈ 𝐴 𝑥