Theorem nfeu1 2635

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

Syntax hints:   ↔ wb 207  ∀wal 1520  ∃wex 1761  Ⅎwnf 1765  ∃!weu 2611

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-10 2112  ax-11 2126  ax-12 2141

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-ex 1762  df-nf 1766  df-mo 2576  df-eu 2612

This theorem is referenced by:  eupicka  2689  2eu8  2716  exists2OLD  2721  nfreu1  3331  eusv2i  5186  eusv2nf  5187  reusv2lem3  5192  iota2  6215  sniota  6216  fv3  6556  tz6.12c  6563  eusvobj1  7010  opiota  7613  dfac5lem5  9399  bnj1366  31718  bnj849  31813  pm14.24  40302  eu2ndop1stv  42840  tz6.12c-afv2  42957  setrec2lem2  44277