Theorem dfint2

Description: Alternate definition of class intersection. (Contributed by NM, 28-Jun-1998)

	Ref	Expression
Assertion	dfint2	$$⊢\bigcap A=\left\{x|\forall y\in Ax\in y\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-int	$$⊢\bigcap A=\left\{x|\forall y\left(y\in A\to x\in y\right)\right\}$$
2		df-ral	$$⊢\forall y\in Ax\in y\leftrightarrow \forall y\left(y\in A\to x\in y\right)$$
3	2	abbii	$$⊢\left\{x|\forall y\in Ax\in y\right\}=\left\{x|\forall y\left(y\in A\to x\in y\right)\right\}$$
4	1 3	eqtr4i	$$⊢\bigcap A=\left\{x|\forall y\in Ax\in y\right\}$$