Theorem nfae 2111

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

Syntax hints:   A.wal 1435   F/wnf 1663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053

This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-nf 1664

This theorem is referenced by:  nfnae  2113  axc16nfALT  2120  dral2  2121  drnf2  2127  sbequ5  2181  sbco3  2211  2ax6elem  2244  sbal  2257  exists1  2359  axi12  2398  axrepnd  9020  axunnd  9022  axpowndlem3  9025  axpownd  9027  axregndlem1  9028  axregnd  9030  axacndlem1  9033  axacndlem2  9034  axacndlem3  9035  axacndlem4  9036  axacndlem5  9037  axacnd  9038