Theorem nfae 2029

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

Assertion

Ref	Expression
nfae	|- F/ z A. x x = y

Proof of Theorem nfae

Step	Hyp	Ref	Expression
1		hbae 2028	. 2 |- ( A. x x = y -> A. z A. x x = y )
2	1	nfi 1606	1 |- F/ z A. x x = y

Syntax hints:   A.wal 1377   F/wnf 1599

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-nf 1600

This theorem is referenced by:  nfnae  2031  ax16nfALT  2038  dral2  2039  drnf2  2045  sbequ5  2101  sbcom2OLD  2174  2ax6elem  2179  sbal  2196  exists1  2398  axi12  2443  copsexgOLD  4733  axrepnd  8965  axunnd  8967  axpowndlem3  8971  axpowndlem3OLD  8972  axpownd  8974  axregndlem1  8975  axregnd  8977  axregndOLD  8978  axacndlem1  8981  axacndlem2  8982  axacndlem3  8983  axacndlem4  8984  axacndlem5  8985  axacnd  8986