Theorem eupick 2358

Description: Existential uniqueness "picks" a variable value for which another wff is true. If there is only one thing such that is true, and there is also an (actually the same one) such that and are both true, then implies regardless of . This theorem can be useful for eliminating existential quantifiers in a hypothesis. Compare Theorem *14.26 in [WhiteheadRussell] p. 192. (Contributed by NM, 10-Jul-1994.)

Assertion

Ref	Expression
eupick

Proof of Theorem eupick

Step	Hyp	Ref	Expression
1		eumo 2313	. 2
2		mopick 2356	. 2
3	1, 2	sylan 471	1

Syntax hints:  ->wi 4  /\wa 369  E.wex 1612  E!weu 2282  E*wmo 2283

This theorem is referenced by:  eupicka  2359  eupickb  2360  reupick  3781  reupick3  3782  eusv2nf  4650  reusv2lem3  4655  copsexg  4737  copsexgOLD  4738  funssres  5633  oprabid  6323  txcn  20127  isch3  26159  iotasbc  31326  bnj849  33983

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-12 1854  ax-13 1999

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617  df-eu 2286  df-mo 2287