Theorem nfnae 2318

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

Assertion

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

Proof of Theorem nfnae

Step	Hyp	Ref	Expression
1		nfae 2316	. 2 |- F/ z A. x x = y
2	1	nfn 1784	1 |- F/ z -. A. x x = y

Syntax hints:   -. wn 3   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:  nfald2  2331  dvelimf  2334  sbequ6  2388  nfsb4t  2389  sbco2  2415  sbco3  2417  sb9  2426  2ax6elem  2449  sbal1  2460  sbal2  2461  axbnd  2601  nfabd2  2784  ralcom2  3104  dfid3  5025  nfriotad  6619  axextnd  9413  axrepndlem1  9414  axrepndlem2  9415  axrepnd  9416  axunndlem1  9417  axunnd  9418  axpowndlem2  9420  axpowndlem3  9421  axpowndlem4  9422  axpownd  9423  axregndlem2  9425  axregnd  9426  axinfndlem1  9427  axinfnd  9428  axacndlem4  9432  axacndlem5  9433  axacnd  9434  axextdist  31705  axext4dist  31706  distel  31709  bj-axc14nf  32838  wl-cbvalnaed  33319  wl-2sb6d  33341  wl-sbalnae  33345  wl-mo2df  33352  wl-mo2tf  33353  wl-eudf  33354  wl-eutf  33355  wl-euequ1f  33356  ax6e2ndeq  38775  ax6e2ndeqVD  39145