eupick - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem eupick 1411

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, which apparently does not appear explicitly in the literature, can be quite useful because it lets us eliminate existential quantifiers in a hypothesis.

**Assertion**
Ref	Expression
eupick	$/\$ $/\$

**Proof of Theorem eupick**
Step	Hyp	Ref	Expression
1		mopick 1410	. 2 $/\$ $/\$
2		eumo 1388	. 2
3	1, 2	sylan 448	1 $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 3 $/\$ wa 223

wex 956

weu 1357

wmo 1358

This theorem is referenced by: eupickb 1412 reupick 2250 funssres 3492 tz6.12-1 3675 chcmh 9264

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-4 951 ax-5 952 ax-6 953 ax-7 954 ax-gen 955 ax-8 1101 ax-9 1102 ax-10 1103 ax-12 1104 ax-11 1180 ax-17 1190 ax-16 1194 ax-11o 1202

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-ex 957 df-sb 1155 df-eu 1359 df-mo 1360