Theorem 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 \mathrm{V}$$
Assertion	inex1	$$⊢A\cap B\in \mathrm{V}$$

Proof

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