Description: Two ways to express "exactly one thing exists". The left-hand side requires only one variable to express this. Both sides are false in set theory, see Theorem dtru . (Contributed by NM, 5-Apr-2004) (Proof shortened by BJ, 7-Oct-2022)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | exists1 | |- ( E! x x = x <-> A. x x = y ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | equid | |- x = x |
|
| 2 | 1 | bitru | |- ( x = x <-> T. ) |
| 3 | 2 | eubii | |- ( E! x x = x <-> E! x T. ) |
| 4 | euae | |- ( E! x T. <-> A. x x = y ) |
|
| 5 | 3 4 | bitri | |- ( E! x x = x <-> A. x x = y ) |