Theorem nfae 2006

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

Syntax hints:   A.wal 1368   F/wnf 1590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591

This theorem is referenced by:  nfnae  2008  ax16nfALT  2020  dral2  2022  drnf2  2028  sbequ5  2084  sbcom2OLD  2158  2ax6elem  2163  sbal  2180  exists1  2382  axi12  2427  copsexgOLD  4661  axrepnd  8845  axunnd  8847  axpowndlem3  8851  axpowndlem3OLD  8852  axpownd  8854  axregndlem1  8855  axregnd  8857  axregndOLD  8858  axacndlem1  8861  axacndlem2  8862  axacndlem3  8863  axacndlem4  8864  axacndlem5  8865  axacnd  8866