Theorem nfeu1 2508

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 2502	. 2 ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
2		nfa1 2068	. . 3 ⊢ Ⅎ𝑥∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
3	2	nfex 2192	. 2 ⊢ Ⅎ𝑥∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
4	1, 3	nfxfr 1819	1 ⊢ Ⅎ𝑥∃!𝑥𝜑

Syntax hints:   ↔ wb 196  ∀wal 1521  ∃wex 1744  Ⅎwnf 1748  ∃!weu 2498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-10 2059  ax-11 2074  ax-12 2087

This theorem depends on definitions:  df-bi 197  df-or 384  df-ex 1745  df-nf 1750  df-eu 2502

This theorem is referenced by:  nfmo1  2509  eupicka  2566  2eu8  2589  exists2  2591  nfreu1  3139  eusv2i  4893  eusv2nf  4894  reusv2lem3  4901  iota2  5915  sniota  5916  fv3  6244  tz6.12c  6251  eusvobj1  6684  opiota  7273  dfac5lem5  8988  bnj1366  31026  bnj849  31121  pm14.24  38950  eu2ndop1stv  41523  setrec2lem2  42766