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	$$⊢\bigcap A=\bigcap _{x\in A}x$$

Proof

Step	Hyp	Ref	Expression
1		dfint2	$$⊢\bigcap A=\left\{y|\forall x\in Ay\in x\right\}$$
2		df-iin	$$⊢\bigcap _{x\in A}x=\left\{y|\forall x\in Ay\in x\right\}$$
3	1 2	eqtr4i	$$⊢\bigcap A=\bigcap _{x\in A}x$$