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 2149 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 1857	1 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦

Syntax hints:  ¬ wn 3  ∀wal 1538  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-10 2141  ax-11 2157  ax-12 2177  ax-13 2377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784

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  2929  ralcom2  3377  dfid3  5581  nfriotad  7399  axextnd  10631  axrepndlem1  10632  axrepndlem2  10633  axrepnd  10634  axunndlem1  10635  axunnd  10636  axpowndlem2  10638  axpowndlem3  10639  axpowndlem4  10640  axpownd  10641  axregndlem2  10643  axregnd  10644  axinfndlem1  10645  axinfnd  10646  axacndlem4  10650  axacndlem5  10651  axacnd  10652  axnulg  35106  axextdist  35800  axextbdist  35801  distel  35804  wl-cbvalnaed  37533  wl-2sb6d  37559  wl-sbalnae  37563  wl-mo2df  37571  wl-mo2tf  37572  wl-eudf  37573  wl-eutf  37574  ax6e2ndeq  44579  ax6e2ndeqVD  44929