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 |
| 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 |