Theorem nfnae 2445

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

Syntax hints:  ¬ wn 3  ∀wal 1536  Ⅎ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 1911  ax-6 1970  ax-7 2015  ax-10 2142  ax-11 2158  ax-12 2175  ax-13 2379

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfald2  2456  dvelimf  2459  sbequ6  2478  2ax6elem  2482  nfsb4t  2517  sbco2  2530  sbco3  2532  sb9  2538  sbal1  2548  sbal2  2549  sbal2OLD  2550  nfsb4tALT  2580  sbco2ALT  2591  nfabd2  2978  ralcom2  3316  dfid3  5427  nfriotad  7104  axextnd  10002  axrepndlem1  10003  axrepndlem2  10004  axrepnd  10005  axunndlem1  10006  axunnd  10007  axpowndlem2  10009  axpowndlem3  10010  axpowndlem4  10011  axpownd  10012  axregndlem2  10014  axregnd  10015  axinfndlem1  10016  axinfnd  10017  axacndlem4  10021  axacndlem5  10022  axacnd  10023  axextdist  33157  axextbdist  33158  distel  33161  wl-cbvalnaed  34937  wl-2sb6d  34959  wl-sbalnae  34963  wl-mo2df  34971  wl-mo2tf  34972  wl-eudf  34973  wl-eutf  34974  ax6e2ndeq  41265  ax6e2ndeqVD  41615