Theorem nfeu1 2586

Description: Bound-variable hypothesis builder for uniqueness. See also nfeu1ALT 2587. (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 2572	. 2 ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
2		nfa1 2156	. . 3 ⊢ Ⅎ𝑥∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
3	2	nfex 2327	. 2 ⊢ Ⅎ𝑥∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
4	1, 3	nfxfr 1854	1 ⊢ Ⅎ𝑥∃!𝑥𝜑

Syntax hints:   ↔ wb 206  ∀wal 1539  ∃wex 1780  Ⅎwnf 1784  ∃!weu 2566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-10 2146  ax-11 2162  ax-12 2182

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-nf 1785  df-mo 2537  df-eu 2567

This theorem is referenced by:  eupicka  2632  2eu8  2657  nfreu1  3376  eusv2i  5337  eusv2nf  5338  reusv2lem3  5343  iota2  6479  sniota  6481  fv3  6850  eusvobj1  7349  opiota  8001  dfac5lem5  10035  bnj1366  34934  bnj849  35030  pm14.24  44615  eu2ndop1stv  47313  tz6.12c-afv2  47430  setrec2lem2  49881