Theorem nfeu1 2581

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

Syntax hints:   ↔ wb 206  ∀wal 1538  ∃wex 1779  Ⅎwnf 1783  ∃!weu 2561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-10 2142  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-nf 1784  df-mo 2533  df-eu 2562

This theorem is referenced by:  eupicka  2627  2eu8  2652  nfreu1  3373  eusv2i  5333  eusv2nf  5334  reusv2lem3  5339  iota2  6471  sniota  6473  fv3  6840  eusvobj1  7342  opiota  7994  dfac5lem5  10021  bnj1366  34796  bnj849  34892  pm14.24  44405  eu2ndop1stv  47109  tz6.12c-afv2  47226  setrec2lem2  49679