Theorem nfeu1 2294

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 2286	. 2
2		nfa1 1897	. . 3
3	2	nfex 1948	. 2
4	1, 3	nfxfr 1645	1

Syntax hints:  <->wb 184  A.wal 1393  E.wex 1612  F/wnf 1616  E!weu 2282

This theorem is referenced by:  nfmo1  2295  eupicka  2359  2eu8  2386  exists2  2389  nfreu1  3028  eusv2i  4649  eusv2nf  4650  reusv2lem3  4655  iota2  5582  sniota  5583  fv3  5884  tz6.12c  5890  eusvobj1  6290  opiota  6859  dfac5lem5  8529  pm14.24  31339  eu2ndop1stv  32207  bnj1366  33888  bnj849  33983

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854

This theorem depends on definitions:  df-bi 185  df-ex 1613  df-nf 1617  df-eu 2286