Description: A condition implying that at least two things exist. (Contributed by NM, 10-Apr-2004) (Proof shortened by Andrew Salmon, 9-Jul-2011) Reduce axiom usage. (Revised by Wolf Lammen, 4-Mar-2023)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | exists2 | |- ( ( E. x ph /\ E. x -. ph ) -> -. E! x x = x ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | axc16nf | |- ( A. x x = y -> F/ x ph ) |
|
| 2 | 1 | nfrd | |- ( A. x x = y -> ( E. x ph -> A. x ph ) ) |
| 3 | 2 | com12 | |- ( E. x ph -> ( A. x x = y -> A. x ph ) ) |
| 4 | exists1 | |- ( E! x x = x <-> A. x x = y ) |
|
| 5 | alex | |- ( A. x ph <-> -. E. x -. ph ) |
|
| 6 | 5 | bicomi | |- ( -. E. x -. ph <-> A. x ph ) |
| 7 | 3 4 6 | 3imtr4g | |- ( E. x ph -> ( E! x x = x -> -. E. x -. ph ) ) |
| 8 | 7 | con2d | |- ( E. x ph -> ( E. x -. ph -> -. E! x x = x ) ) |
| 9 | 8 | imp | |- ( ( E. x ph /\ E. x -. ph ) -> -. E! x x = x ) |