# Metamath Proof Explorer

## 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}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}↔\left({y}\in {A}\wedge {y}\in {B}\right)\right)$
3 dfcleq ${⊢}{x}={A}\cap {B}↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}↔{y}\in \left({A}\cap {B}\right)\right)$
4 elin ${⊢}{y}\in \left({A}\cap {B}\right)↔\left({y}\in {A}\wedge {y}\in {B}\right)$
5 4 bibi2i ${⊢}\left({y}\in {x}↔{y}\in \left({A}\cap {B}\right)\right)↔\left({y}\in {x}↔\left({y}\in {A}\wedge {y}\in {B}\right)\right)$
6 5 albii ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}↔{y}\in \left({A}\cap {B}\right)\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}↔\left({y}\in {A}\wedge {y}\in {B}\right)\right)$
7 3 6 bitri ${⊢}{x}={A}\cap {B}↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}↔\left({y}\in {A}\wedge {y}\in {B}\right)\right)$
8 7 exbii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{x}={A}\cap {B}↔\exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {x}↔\left({y}\in {A}\wedge {y}\in {B}\right)\right)$
9 2 8 mpbir ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{x}={A}\cap {B}$
10 9 issetri ${⊢}{A}\cap {B}\in \mathrm{V}$