# Metamath Proof Explorer

## Theorem elnev

Description: Any set that contains one element less than the universe is not equal to it. (Contributed by Andrew Salmon, 16-Jun-2011)

Ref Expression
Assertion elnev ${⊢}{A}\in \mathrm{V}↔\left\{{x}|¬{x}={A}\right\}\ne \mathrm{V}$

### Proof

Step Hyp Ref Expression
1 isset ${⊢}{A}\in \mathrm{V}↔\exists {x}\phantom{\rule{.4em}{0ex}}{x}={A}$
2 df-v ${⊢}\mathrm{V}=\left\{{x}|{x}={x}\right\}$
3 2 eqeq2i ${⊢}\left\{{x}|¬{x}={A}\right\}=\mathrm{V}↔\left\{{x}|¬{x}={A}\right\}=\left\{{x}|{x}={x}\right\}$
4 equid ${⊢}{x}={x}$
5 4 tbt ${⊢}¬{x}={A}↔\left(¬{x}={A}↔{x}={x}\right)$
6 5 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}¬{x}={A}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left(¬{x}={A}↔{x}={x}\right)$
7 alnex ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}¬{x}={A}↔¬\exists {x}\phantom{\rule{.4em}{0ex}}{x}={A}$
8 abbi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(¬{x}={A}↔{x}={x}\right)↔\left\{{x}|¬{x}={A}\right\}=\left\{{x}|{x}={x}\right\}$
9 6 7 8 3bitr3ri ${⊢}\left\{{x}|¬{x}={A}\right\}=\left\{{x}|{x}={x}\right\}↔¬\exists {x}\phantom{\rule{.4em}{0ex}}{x}={A}$
10 3 9 bitri ${⊢}\left\{{x}|¬{x}={A}\right\}=\mathrm{V}↔¬\exists {x}\phantom{\rule{.4em}{0ex}}{x}={A}$
11 10 necon2abii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{x}={A}↔\left\{{x}|¬{x}={A}\right\}\ne \mathrm{V}$
12 1 11 bitri ${⊢}{A}\in \mathrm{V}↔\left\{{x}|¬{x}={A}\right\}\ne \mathrm{V}$