Theorem nfeu1 2583

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

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

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 2144  ax-11 2160  ax-12 2180

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

This theorem is referenced by:  eupicka  2629  2eu8  2654  nfreu1  3374  eusv2i  5330  eusv2nf  5331  reusv2lem3  5336  iota2  6470  sniota  6472  fv3  6840  eusvobj1  7339  opiota  7991  dfac5lem5  10018  bnj1366  34841  bnj849  34937  pm14.24  44535  eu2ndop1stv  47235  tz6.12c-afv2  47352  setrec2lem2  49805