Theorem nfeu1 2479

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 2473	. 2 ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
2		nfa1 2025	. . 3 ⊢ Ⅎ𝑥∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
3	2	nfex 2151	. 2 ⊢ Ⅎ𝑥∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
4	1, 3	nfxfr 1776	1 ⊢ Ⅎ𝑥∃!𝑥𝜑

Syntax hints:   ↔ wb 196  ∀wal 1478  ∃wex 1701  Ⅎwnf 1705  ∃!weu 2469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-10 2016  ax-11 2031  ax-12 2044

This theorem depends on definitions:  df-bi 197  df-or 385  df-ex 1702  df-nf 1707  df-eu 2473

This theorem is referenced by:  nfmo1  2480  eupicka  2536  2eu8  2559  exists2  2561  nfreu1  3100  eusv2i  4823  eusv2nf  4824  reusv2lem3  4831  iota2  5836  sniota  5837  fv3  6163  tz6.12c  6170  eusvobj1  6598  opiota  7174  dfac5lem5  8894  bnj1366  30605  bnj849  30700  pm14.24  38112  eu2ndop1stv  40503  setrec2lem2  41731