# 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
`|- -. A. x x = y`

### Proof

Step Hyp Ref Expression
1 el
` |-  E. w x e. w`
2 ax-nul
` |-  E. z A. x -. x e. z`
3 sp
` |-  ( A. x -. x e. z -> -. x e. z )`
4 2 3 eximii
` |-  E. z -. x e. z`
5 exdistrv
` |-  ( E. w E. z ( x e. w /\ -. x e. z ) <-> ( E. w x e. w /\ E. z -. x e. z ) )`
6 1 4 5 mpbir2an
` |-  E. w E. z ( x e. w /\ -. x e. z )`
7 ax9v2
` |-  ( w = z -> ( x e. w -> x e. z ) )`
8 7 com12
` |-  ( x e. w -> ( w = z -> x e. z ) )`
9 8 con3dimp
` |-  ( ( x e. w /\ -. x e. z ) -> -. w = z )`
10 9 2eximi
` |-  ( E. w E. z ( x e. w /\ -. x e. z ) -> E. w E. z -. w = z )`
11 equequ2
` |-  ( z = y -> ( w = z <-> w = y ) )`
12 11 notbid
` |-  ( z = y -> ( -. w = z <-> -. w = y ) )`
13 nfv
` |-  F/ x -. w = y`
14 ax7v1
` |-  ( x = w -> ( x = y -> w = y ) )`
15 14 con3d
` |-  ( x = w -> ( -. w = y -> -. x = y ) )`
16 13 15 spimefv
` |-  ( -. w = y -> E. x -. x = y )`
17 12 16 syl6bi
` |-  ( z = y -> ( -. w = z -> E. x -. x = y ) )`
18 nfv
` |-  F/ x -. z = y`
19 ax7v1
` |-  ( x = z -> ( x = y -> z = y ) )`
20 19 con3d
` |-  ( x = z -> ( -. z = y -> -. x = y ) )`
21 18 20 spimefv
` |-  ( -. z = y -> E. x -. x = y )`
22 21 a1d
` |-  ( -. z = y -> ( -. w = z -> E. x -. x = y ) )`
23 17 22 pm2.61i
` |-  ( -. w = z -> E. x -. x = y )`
24 23 exlimivv
` |-  ( E. w E. z -. w = z -> E. x -. x = y )`
25 6 10 24 mp2b
` |-  E. x -. x = y`
26 exnal
` |-  ( E. x -. x = y <-> -. A. x x = y )`
27 25 26 mpbi
` |-  -. A. x x = y`