This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 V$

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