Theorem nfeu1 2674

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

Syntax hints:   ↔ wb 208  ∀wal 1535  ∃wex 1780  Ⅎwnf 1784  ∃!weu 2653

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 1970  ax-7 2015  ax-10 2145  ax-11 2161  ax-12 2177

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1781  df-nf 1785  df-mo 2622  df-eu 2654

This theorem is referenced by:  eupicka  2719  2eu8  2744  nfreu1  3372  eusv2i  5297  eusv2nf  5298  reusv2lem3  5303  iota2  6346  sniota  6348  fv3  6690  tz6.12c  6697  eusvobj1  7152  opiota  7759  dfac5lem5  9555  bnj1366  32103  bnj849  32199  pm14.24  40771  eu2ndop1stv  43331  tz6.12c-afv2  43448  setrec2lem2  44804