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  3349  dfid3  5532  nfriotad  7338  axextnd  10516  axrepndlem1  10517  axrepndlem2  10518  axrepnd  10519  axunndlem1  10520  axunnd  10521  axpowndlem2  10523  axpowndlem3  10524  axpowndlem4  10525  axpownd  10526  axregndlem2  10528  axregnd  10529  axinfndlem1  10530  axinfnd  10531  axacndlem4  10535  axacndlem5  10536  axacnd  10537  axnulg  35291  axextdist  36019  axextbdist  36020  distel  36023  mh-setindnd  36695  wl-cbvalnaed  37816  wl-2sb6d  37842  wl-sbalnae  37846  wl-mo2df  37854  wl-mo2tf  37855  wl-eudf  37856  wl-eutf  37857  ax6e2ndeq  44944  ax6e2ndeqVD  45293