Theorem nfnae 2464

Description: All variables are effectively bound in a distinct variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2402. Use the weaker nfnaew 2182 when possible. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.)

Assertion

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

Proof of Theorem nfnae

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

Syntax hints:  ¬ wn 3  ∀wal 1566  Ⅎwnf 1811

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-10 2174  ax-11 2190  ax-12 2211  ax-13 2402

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1571  df-ex 1808  df-nf 1812

This theorem is referenced by:  nfald2  2475  dvelimf  2478  sbequ6  2496  2ax6elem  2500  nfsb4t  2529  sbco2  2541  sbco3  2543  sb9  2549  sbal1  2558  sbal2  2559  nfabd2  2946  ralcom2  3364  dfid3  5559  nfriotad  7378  axextnd  10575  axrepndlem1  10576  axrepndlem2  10577  axrepnd  10578  axunndlem1  10579  axunnd  10580  axpowndlem2  10582  axpowndlem3  10583  axpowndlem4  10584  axpownd  10585  axregndlem2  10587  axregnd  10588  axinfndlem1  10589  axinfnd  10590  axacndlem4  10594  axacndlem5  10595  axacnd  10596  axsepg2  35507  axsepg5  35511  axnulg  35512  axpowg2  35514  axpowg3  35515  axextdist  36243  axextbdist  36244  distel  36247  axtcond  36933  mh-setindnd  36992  wl-cbvalnaed  38131  wl-2sb6d  38157  wl-sbalnae  38161  wl-mo2df  38169  wl-mo2tf  38170  wl-eudf  38171  wl-eutf  38172  ax6e2ndeq  45216  ax6e2ndeqVD  45565