Theorem nfae 2316

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 2315	. 2 |- ( A. x x = y -> A. z A. x x = y )
2	1	nf5i 2024	1 |- F/ z A. x x = y

Syntax hints:   A.wal 1481   F/wnf 1708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710

This theorem is referenced by:  nfnae  2318  axc16nfALT  2323  dral2  2324  drnf2  2330  sbequ5  2387  sbco3  2417  2ax6elem  2449  sbal  2462  exists1  2561  axi12  2600  axrepnd  9416  axunnd  9418  axpowndlem3  9421  axpownd  9423  axregndlem1  9424  axregnd  9426  axacndlem1  9429  axacndlem2  9430  axacndlem3  9431  axacndlem4  9432  axacndlem5  9433  axacnd  9434