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  3384  eusv2i  5349  eusv2nf  5350  reusv2lem3  5355  iota2  6500  sniota  6502  fv3  6876  tz6.12cOLD  6885  eusvobj1  7380  opiota  8038  dfac5lem5  10080  bnj1366  34819  bnj849  34915  pm14.24  44421  eu2ndop1stv  47123  tz6.12c-afv2  47240  setrec2lem2  49680