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  3340  dfid3  5524  nfriotad  7330  axextnd  10509  axrepndlem1  10510  axrepndlem2  10511  axrepnd  10512  axunndlem1  10513  axunnd  10514  axpowndlem2  10516  axpowndlem3  10517  axpowndlem4  10518  axpownd  10519  axregndlem2  10521  axregnd  10522  axinfndlem1  10523  axinfnd  10524  axacndlem4  10528  axacndlem5  10529  axacnd  10530  axnulg  35271  axextdist  35999  axextbdist  36000  distel  36003  axtcond  36680  mh-setindnd  36739  wl-cbvalnaed  37877  wl-2sb6d  37903  wl-sbalnae  37907  wl-mo2df  37915  wl-mo2tf  37916  wl-eudf  37917  wl-eutf  37918  ax6e2ndeq  45010  ax6e2ndeqVD  45359