# Metamath Proof Explorer

## Theorem dtru

Description: At least two sets exist (or in terms of first-order logic, the universe of discourse has two or more objects). Note that we may not substitute the same variable for both x and y (as indicated by the distinct variable requirement), for otherwise we would contradict stdpc6 .

This theorem is proved directly from set theory axioms (no set theory definitions) and does not use ax-ext or ax-sep . See dtruALT for a shorter proof using these axioms.

The proof makes use of dummy variables z and w which do not appear in the final theorem. They must be distinct from each other and from x and y . In other words, if we were to substitute x for z throughout the proof, the proof would fail. (Contributed by NM, 7-Nov-2006) Avoid ax-13 . (Revised by Gino Giotto, 5-Sep-2023)

Ref Expression
Assertion dtru ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$

### Proof

Step Hyp Ref Expression
1 el ${⊢}\exists {w}\phantom{\rule{.4em}{0ex}}{x}\in {w}$
2 ax-nul ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}¬{x}\in {z}$
3 sp ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}¬{x}\in {z}\to ¬{x}\in {z}$
4 2 3 eximii ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}¬{x}\in {z}$
5 exdistrv ${⊢}\exists {w}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge ¬{x}\in {z}\right)↔\left(\exists {w}\phantom{\rule{.4em}{0ex}}{x}\in {w}\wedge \exists {z}\phantom{\rule{.4em}{0ex}}¬{x}\in {z}\right)$
6 1 4 5 mpbir2an ${⊢}\exists {w}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge ¬{x}\in {z}\right)$
7 ax9v2 ${⊢}{w}={z}\to \left({x}\in {w}\to {x}\in {z}\right)$
8 7 com12 ${⊢}{x}\in {w}\to \left({w}={z}\to {x}\in {z}\right)$
9 8 con3dimp ${⊢}\left({x}\in {w}\wedge ¬{x}\in {z}\right)\to ¬{w}={z}$
10 9 2eximi ${⊢}\exists {w}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}\in {w}\wedge ¬{x}\in {z}\right)\to \exists {w}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}¬{w}={z}$
11 equequ2 ${⊢}{z}={y}\to \left({w}={z}↔{w}={y}\right)$
12 11 notbid ${⊢}{z}={y}\to \left(¬{w}={z}↔¬{w}={y}\right)$
13 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}¬{w}={y}$
14 ax7v1 ${⊢}{x}={w}\to \left({x}={y}\to {w}={y}\right)$
15 14 con3d ${⊢}{x}={w}\to \left(¬{w}={y}\to ¬{x}={y}\right)$
16 13 15 spimefv ${⊢}¬{w}={y}\to \exists {x}\phantom{\rule{.4em}{0ex}}¬{x}={y}$
17 12 16 syl6bi ${⊢}{z}={y}\to \left(¬{w}={z}\to \exists {x}\phantom{\rule{.4em}{0ex}}¬{x}={y}\right)$
18 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}¬{z}={y}$
19 ax7v1 ${⊢}{x}={z}\to \left({x}={y}\to {z}={y}\right)$
20 19 con3d ${⊢}{x}={z}\to \left(¬{z}={y}\to ¬{x}={y}\right)$
21 18 20 spimefv ${⊢}¬{z}={y}\to \exists {x}\phantom{\rule{.4em}{0ex}}¬{x}={y}$
22 21 a1d ${⊢}¬{z}={y}\to \left(¬{w}={z}\to \exists {x}\phantom{\rule{.4em}{0ex}}¬{x}={y}\right)$
23 17 22 pm2.61i ${⊢}¬{w}={z}\to \exists {x}\phantom{\rule{.4em}{0ex}}¬{x}={y}$
24 23 exlimivv ${⊢}\exists {w}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}¬{w}={z}\to \exists {x}\phantom{\rule{.4em}{0ex}}¬{x}={y}$
25 6 10 24 mp2b ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}¬{x}={y}$
26 exnal ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}¬{x}={y}↔¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
27 25 26 mpbi ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$