Theorem nfnae 2434

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

Syntax hints:  ¬ wn 3  ∀wal 1537  Ⅎwnf 1787

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-10 2139  ax-11 2156  ax-12 2173  ax-13 2372

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-nf 1788

This theorem is referenced by:  nfald2  2445  dvelimf  2448  sbequ6  2466  2ax6elem  2470  nfsb4t  2503  sbco2  2515  sbco3  2517  sb9  2523  sbal1  2533  sbal2  2534  nfabd2  2932  ralcom2  3288  dfid3  5483  nfriotad  7224  axextnd  10278  axrepndlem1  10279  axrepndlem2  10280  axrepnd  10281  axunndlem1  10282  axunnd  10283  axpowndlem2  10285  axpowndlem3  10286  axpowndlem4  10287  axpownd  10288  axregndlem2  10290  axregnd  10291  axinfndlem1  10292  axinfnd  10293  axacndlem4  10297  axacndlem5  10298  axacnd  10299  axextdist  33681  axextbdist  33682  distel  33685  wl-cbvalnaed  35618  wl-2sb6d  35640  wl-sbalnae  35644  wl-mo2df  35652  wl-mo2tf  35653  wl-eudf  35654  wl-eutf  35655  ax6e2ndeq  42068  ax6e2ndeqVD  42418