Theorem nfnae 2433

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

Syntax hints:  ¬ wn 3  ∀wal 1539  Ⅎ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 1913  ax-6 1971  ax-7 2011  ax-10 2137  ax-11 2154  ax-12 2171  ax-13 2371

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfald2  2444  dvelimf  2447  sbequ6  2465  2ax6elem  2469  nfsb4t  2498  sbco2  2510  sbco3  2512  sb9  2518  sbal1  2527  sbal2  2528  nfabd2  2929  ralcom2  3373  dfid3  5577  nfriotad  7376  axextnd  10585  axrepndlem1  10586  axrepndlem2  10587  axrepnd  10588  axunndlem1  10589  axunnd  10590  axpowndlem2  10592  axpowndlem3  10593  axpowndlem4  10594  axpownd  10595  axregndlem2  10597  axregnd  10598  axinfndlem1  10599  axinfnd  10600  axacndlem4  10604  axacndlem5  10605  axacnd  10606  axextdist  34766  axextbdist  34767  distel  34770  wl-cbvalnaed  36396  wl-2sb6d  36418  wl-sbalnae  36422  wl-mo2df  36430  wl-mo2tf  36431  wl-eudf  36432  wl-eutf  36433  ax6e2ndeq  43310  ax6e2ndeqVD  43660