Theorem nfeu1 2591

Description: Bound-variable hypothesis builder for uniqueness. See also nfeu1ALT 2592. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 7-Oct-2016.)

Assertion

Ref	Expression
nfeu1	⊢ Ⅎ𝑥∃!𝑥𝜑

Proof of Theorem nfeu1

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eu6 2577	. 2 ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
2		nfa1 2152	. . 3 ⊢ Ⅎ𝑥∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
3	2	nfex 2328	. 2 ⊢ Ⅎ𝑥∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
4	1, 3	nfxfr 1851	1 ⊢ Ⅎ𝑥∃!𝑥𝜑

Syntax hints:   ↔ wb 206  ∀wal 1535  ∃wex 1777  Ⅎwnf 1781  ∃!weu 2571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-10 2141  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-nf 1782  df-mo 2543  df-eu 2572

This theorem is referenced by:  eupicka  2637  2eu8  2662  nfreu1  3420  eusv2i  5412  eusv2nf  5413  reusv2lem3  5418  iota2  6562  sniota  6564  fv3  6938  tz6.12cOLD  6947  eusvobj1  7441  opiota  8100  dfac5lem5  10196  bnj1366  34805  bnj849  34901  pm14.24  44401  eu2ndop1stv  47040  tz6.12c-afv2  47157  setrec2lem2  48786