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