Theorem nfnae 2439

Description: All variables are effectively bound in a distinct variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2377. Use the weaker nfnaew 2155 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 2438	. 2 ⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦
2	1	nfn 1859	1 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦

Syntax hints:  ¬ wn 3  ∀wal 1540  Ⅎwnf 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-10 2147  ax-11 2163  ax-12 2185  ax-13 2377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfald2  2450  dvelimf  2453  sbequ6  2471  2ax6elem  2475  nfsb4t  2504  sbco2  2516  sbco3  2518  sb9  2524  sbal1  2533  sbal2  2534  nfabd2  2923  ralcom2  3348  dfid3  5523  nfriotad  7328  axextnd  10506  axrepndlem1  10507  axrepndlem2  10508  axrepnd  10509  axunndlem1  10510  axunnd  10511  axpowndlem2  10513  axpowndlem3  10514  axpowndlem4  10515  axpownd  10516  axregndlem2  10518  axregnd  10519  axinfndlem1  10520  axinfnd  10521  axacndlem4  10525  axacndlem5  10526  axacnd  10527  axnulg  35266  axextdist  35993  axextbdist  35994  distel  35997  mh-setindnd  36669  wl-cbvalnaed  37739  wl-2sb6d  37765  wl-sbalnae  37769  wl-mo2df  37777  wl-mo2tf  37778  wl-eudf  37779  wl-eutf  37780  ax6e2ndeq  44867  ax6e2ndeqVD  45216