Metamath Proof Explorer


Theorem exists2

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 )

Proof

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 )