Theorem nfae 2056

Description: All variables are effectively bound in an identical variable specifier. (Contributed by Mario Carneiro, 11-Aug-2016.)

Assertion

Ref	Expression
nfae

Proof of Theorem nfae

Step	Hyp	Ref	Expression
1		hbae 2055	. 2
2	1	nfi 1623	1

Syntax hints:  A.wal 1393  F/wnf 1616

This theorem is referenced by:  nfnae  2058  ax16nfALT  2065  dral2  2066  drnf2  2072  sbequ5  2128  sbco3  2160  2ax6elem  2193  sbal  2206  exists1  2388  axi12  2433  copsexgOLD  4738  axrepnd  8990  axunnd  8992  axpowndlem3  8996  axpowndlem3OLD  8997  axpownd  8999  axregndlem1  9000  axregnd  9002  axregndOLD  9003  axacndlem1  9006  axacndlem2  9007  axacndlem3  9008  axacndlem4  9009  axacndlem5  9010  axacnd  9011

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  ax-13 1999

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617