# Metamath Proof Explorer

## Theorem dfin2

Description: An alternate definition of the intersection of two classes in terms of class difference, requiring no dummy variables. See comments under dfun2 . Another version is given by dfin4 . (Contributed by NM, 10-Jun-2004)

Ref Expression
Assertion dfin2 ${⊢}{A}\cap {B}={A}\setminus \left(\mathrm{V}\setminus {B}\right)$

### Proof

Step Hyp Ref Expression
1 vex ${⊢}{x}\in \mathrm{V}$
2 eldif ${⊢}{x}\in \left(\mathrm{V}\setminus {B}\right)↔\left({x}\in \mathrm{V}\wedge ¬{x}\in {B}\right)$
3 1 2 mpbiran ${⊢}{x}\in \left(\mathrm{V}\setminus {B}\right)↔¬{x}\in {B}$
4 3 con2bii ${⊢}{x}\in {B}↔¬{x}\in \left(\mathrm{V}\setminus {B}\right)$
5 4 anbi2i ${⊢}\left({x}\in {A}\wedge {x}\in {B}\right)↔\left({x}\in {A}\wedge ¬{x}\in \left(\mathrm{V}\setminus {B}\right)\right)$
6 eldif ${⊢}{x}\in \left({A}\setminus \left(\mathrm{V}\setminus {B}\right)\right)↔\left({x}\in {A}\wedge ¬{x}\in \left(\mathrm{V}\setminus {B}\right)\right)$
7 5 6 bitr4i ${⊢}\left({x}\in {A}\wedge {x}\in {B}\right)↔{x}\in \left({A}\setminus \left(\mathrm{V}\setminus {B}\right)\right)$
8 7 ineqri ${⊢}{A}\cap {B}={A}\setminus \left(\mathrm{V}\setminus {B}\right)$