Theorem nfae 2060

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 2059	. 2 |- ( A. x x = y -> A. z A. x x = y )
2	1	nfi 1628	1 |- F/ z A. x x = y

Syntax hints:   A.wal 1396   F/wnf 1621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004

This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-nf 1622

This theorem is referenced by:  nfnae  2062  ax16nfALT  2069  dral2  2070  drnf2  2076  sbequ5  2130  sbco3  2162  2ax6elem  2195  sbal  2208  exists1  2385  axi12  2430  axrepnd  8960  axunnd  8962  axpowndlem3  8965  axpownd  8967  axregndlem1  8968  axregnd  8970  axregndOLD  8971  axacndlem1  8974  axacndlem2  8975  axacndlem3  8976  axacndlem4  8977  axacndlem5  8978  axacnd  8979