Theorem nfeu1 2608

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

Syntax hints:   ↔ wb 209  ∀wal 1536  ∃wex 1781  Ⅎwnf 1785  ∃!weu 2587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-10 2142  ax-11 2158  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-mo 2557  df-eu 2588

This theorem is referenced by:  eupicka  2655  2eu8  2680  nfreu1  3288  eusv2i  5263  eusv2nf  5264  reusv2lem3  5269  iota2  6324  sniota  6326  fv3  6676  tz6.12c  6683  eusvobj1  7144  opiota  7761  dfac5lem5  9587  bnj1366  32329  bnj849  32425  pm14.24  41509  eu2ndop1stv  44049  tz6.12c-afv2  44166  setrec2lem2  45615