Theorem nfnae 2317

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

Assertion

Ref	Expression
nfnae	⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦

Proof of Theorem nfnae

Step	Hyp	Ref	Expression
1		nfae 2315	. 2 ⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦
2	1	nfn 1781	1 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦

Syntax hints:  ¬ wn 3  ∀wal 1478  Ⅎwnf 1705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707

This theorem is referenced by:  nfald2  2330  dvelimf  2333  sbequ6  2387  nfsb4t  2388  sbco2  2414  sbco3  2416  sb9  2425  2ax6elem  2448  sbal1  2459  sbal2  2460  axbnd  2600  nfabd2  2780  ralcom2  3098  dfid3  5000  nfriotad  6584  axextnd  9373  axrepndlem1  9374  axrepndlem2  9375  axrepnd  9376  axunndlem1  9377  axunnd  9378  axpowndlem2  9380  axpowndlem3  9381  axpowndlem4  9382  axpownd  9383  axregndlem2  9385  axregnd  9386  axinfndlem1  9387  axinfnd  9388  axacndlem4  9392  axacndlem5  9393  axacnd  9394  axextdist  31459  axext4dist  31460  distel  31463  bj-axc14nf  32536  wl-cbvalnaed  32990  wl-2sb6d  33012  wl-sbalnae  33016  wl-mo2df  33023  wl-mo2tf  33024  wl-eudf  33025  wl-eutf  33026  wl-euequ1f  33027  ax6e2ndeq  38296  ax6e2ndeqVD  38667