Theorem nfeu1 2609

Description: Bound-variable hypothesis builder for uniqueness. (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		df-eu 2603	. 2 ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
2		nfa1 2169	. . 3 ⊢ Ⅎ𝑥∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
3	2	nfex 2293	. 2 ⊢ Ⅎ𝑥∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
4	1, 3	nfxfr 1920	1 ⊢ Ⅎ𝑥∃!𝑥𝜑

Syntax hints:   ↔ wb 196  ∀wal 1622  ∃wex 1845  Ⅎwnf 1849  ∃!weu 2599

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-10 2160  ax-11 2175  ax-12 2188

This theorem depends on definitions:  df-bi 197  df-or 384  df-ex 1846  df-nf 1851  df-eu 2603

This theorem is referenced by:  nfmo1  2610  eupicka  2667  2eu8  2690  exists2  2692  nfreu1  3240  eusv2i  5004  eusv2nf  5005  reusv2lem3  5012  iota2  6030  sniota  6031  fv3  6359  tz6.12c  6366  eusvobj1  6799  opiota  7388  dfac5lem5  9132  bnj1366  31199  bnj849  31294  pm14.24  39127  eu2ndop1stv  41700  setrec2lem2  42943