inex1

Description: Separation Scheme (Aussonderung) using class notation. Compare Exercise 4 of TakeutiZaring p. 22. (Contributed by NM, 21-Jun-1993)

		Ref	Expression
	Hypothesis	inex1.1	$⊢ A \in V$
	Assertion	inex1	$⊢ A \cap B \in V$

Step	Hyp	Ref	Expression
1		inex1.1	$⊢ A \in V$
2	1	zfauscl	$⊢ \exists x \forall y (y \in x \leftrightarrow (y \in A \land y \in B))$
3		dfcleq	$⊢ x = A \cap B \leftrightarrow \forall y (y \in x \leftrightarrow y \in (A \cap B))$
4		elin	$⊢ y \in (A \cap B) \leftrightarrow (y \in A \land y \in B)$
5	4	bibi2i	$⊢ (y \in x \leftrightarrow y \in (A \cap B)) \leftrightarrow (y \in x \leftrightarrow (y \in A \land y \in B))$
6	5	albii	$⊢ \forall y (y \in x \leftrightarrow y \in (A \cap B)) \leftrightarrow \forall y (y \in x \leftrightarrow (y \in A \land y \in B))$
7	3 6	bitri	$⊢ x = A \cap B \leftrightarrow \forall y (y \in x \leftrightarrow (y \in A \land y \in B))$
8	7	exbii	$⊢ \exists x x = A \cap B \leftrightarrow \exists x \forall y (y \in x \leftrightarrow (y \in A \land y \in B))$
9	2 8	mpbir	$⊢ \exists x x = A \cap B$
10	9	issetri	$⊢ A \cap B \in V$

Metamath Proof Explorer