Theorem nfeu1 2480

Description: Bound-variable hypothesis builder for uniqueness. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 7-Oct-2016.)

Assertion

Ref	Expression
nfeu1	|- F/ x E! x ph

Proof of Theorem nfeu1

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-eu 2474	. 2 |- ( E! x ph <-> E. y A. x ( ph <-> x = y ) )
2		nfa1 2028	. . 3 |- F/ x A. x ( ph <-> x = y )
3	2	nfex 2154	. 2 |- F/ x E. y A. x ( ph <-> x = y )
4	1, 3	nfxfr 1779	1 |- F/ x E! x ph

Syntax hints:   <-> wb 196   A.wal 1481   E.wex 1704   F/wnf 1708   E!weu 2470

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-11 2034  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-or 385  df-ex 1705  df-nf 1710  df-eu 2474

This theorem is referenced by:  nfmo1  2481  eupicka  2537  2eu8  2560  exists2  2562  nfreu1  3110  eusv2i  4863  eusv2nf  4864  reusv2lem3  4871  iota2  5877  sniota  5878  fv3  6206  tz6.12c  6213  eusvobj1  6644  opiota  7229  dfac5lem5  8950  bnj1366  30900  bnj849  30995  pm14.24  38633  eu2ndop1stv  41202  setrec2lem2  42441