Theorem nfeu1 2631

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 2625	. 2 ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
2		nfa1 2187	. . 3 ⊢ Ⅎ𝑥∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
3	2	nfex 2321	. 2 ⊢ Ⅎ𝑥∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
4	1, 3	nfxfr 1932	1 ⊢ Ⅎ𝑥∃!𝑥𝜑

Syntax hints:   ↔ wb 197  ∀wal 1632  ∃wex 1855  Ⅎwnf 1859  ∃!weu 2621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-10 2177  ax-11 2193  ax-12 2206

This theorem depends on definitions:  df-bi 198  df-or 864  df-ex 1856  df-nf 1861  df-eu 2625

This theorem is referenced by:  nfmo1  2632  eupicka  2689  2eu8  2712  exists2  2714  nfreu1  3262  eusv2i  5008  eusv2nf  5009  reusv2lem3  5014  iota2  6031  sniota  6032  fv3  6364  tz6.12c  6371  eusvobj1  6806  opiota  7399  dfac5lem5  9171  bnj1366  31255  bnj849  31350  pm14.24  39172  eu2ndop1stv  41747  setrec2lem2  42993