Theorem inex1g

Description: Closed-form, generalized Separation Scheme. (Contributed by NM, 7-Apr-1995)

	Ref	Expression
Assertion	inex1g	$$⊢A\in V\to A\cap B\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		ineq1	$$⊢x=A\to x\cap B=A\cap B$$
2	1	eleq1d	$$⊢x=A\to \left(x\cap B\in \mathrm{V}\leftrightarrow A\cap B\in \mathrm{V}\right)$$
3		vex	$$⊢x\in \mathrm{V}$$
4	3	inex1	$$⊢x\cap B\in \mathrm{V}$$
5	2 4	vtoclg	$$⊢A\in V\to A\cap B\in \mathrm{V}$$