Theorem nfeu1 2468

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 2462	. 2 ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
2		nfa1 2015	. . 3 ⊢ Ⅎ𝑥∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
3	2	nfex 2140	. 2 ⊢ Ⅎ𝑥∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
4	1, 3	nfxfr 1771	1 ⊢ Ⅎ𝑥∃!𝑥𝜑

Syntax hints:   ↔ wb 195  ∀wal 1473  ∃wex 1695  Ⅎwnf 1699  ∃!weu 2458

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034

This theorem depends on definitions:  df-bi 196  df-or 384  df-ex 1696  df-nf 1701  df-eu 2462

This theorem is referenced by:  nfmo1  2469  eupicka  2525  2eu8  2548  exists2  2550  nfreu1  3089  eusv2i  4789  eusv2nf  4790  reusv2lem3  4797  iota2  5794  sniota  5795  fv3  6116  tz6.12c  6123  eusvobj1  6543  opiota  7118  dfac5lem5  8833  bnj1366  30154  bnj849  30249  pm14.24  37655  eu2ndop1stv  39851  setrec2lem2  42240