Theorem elintrab

Description: Membership in the intersection of a class abstraction. (Contributed by NM, 17-Oct-1999)

	Ref	Expression
Hypothesis	elintab.ex	$$⊢A\in \mathrm{V}$$
Assertion	elintrab	$$⊢A\in \bigcap \left\{x\in B|\phi \right\}\leftrightarrow \forall x\in B\left(\phi \to A\in x\right)$$

Proof

Step	Hyp	Ref	Expression
1		elintab.ex	$$⊢A\in \mathrm{V}$$
2	1	elintab	$$⊢A\in \bigcap \left\{x|\left(x\in B\wedge \phi \right)\right\}\leftrightarrow \forall x\left(\left(x\in B\wedge \phi \right)\to A\in x\right)$$
3		impexp	$$⊢\left(\left(x\in B\wedge \phi \right)\to A\in x\right)\leftrightarrow \left(x\in B\to \left(\phi \to A\in x\right)\right)$$
4	3	albii	$$⊢\forall x\left(\left(x\in B\wedge \phi \right)\to A\in x\right)\leftrightarrow \forall x\left(x\in B\to \left(\phi \to A\in x\right)\right)$$
5	2 4	bitri	$$⊢A\in \bigcap \left\{x|\left(x\in B\wedge \phi \right)\right\}\leftrightarrow \forall x\left(x\in B\to \left(\phi \to A\in x\right)\right)$$
6		df-rab	$$⊢\left\{x\in B|\phi \right\}=\left\{x|\left(x\in B\wedge \phi \right)\right\}$$
7	6	inteqi	$$⊢\bigcap \left\{x\in B|\phi \right\}=\bigcap \left\{x|\left(x\in B\wedge \phi \right)\right\}$$
8	7	eleq2i	$$⊢A\in \bigcap \left\{x\in B|\phi \right\}\leftrightarrow A\in \bigcap \left\{x|\left(x\in B\wedge \phi \right)\right\}$$
9		df-ral	$$⊢\forall x\in B\left(\phi \to A\in x\right)\leftrightarrow \forall x\left(x\in B\to \left(\phi \to A\in x\right)\right)$$
10	5 8 9	3bitr4i	$$⊢A\in \bigcap \left\{x\in B|\phi \right\}\leftrightarrow \forall x\in B\left(\phi \to A\in x\right)$$