Theorem nfnae 2437

Description: All variables are effectively bound in a distinct variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2375. 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 2436	. 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 2184  ax-13 2375

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  2448  dvelimf  2451  sbequ6  2469  2ax6elem  2473  nfsb4t  2502  sbco2  2514  sbco3  2516  sb9  2522  sbal1  2531  sbal2  2532  nfabd2  2920  ralcom2  3337  dfid3  5518  nfriotad  7324  axextnd  10503  axrepndlem1  10504  axrepndlem2  10505  axrepnd  10506  axunndlem1  10507  axunnd  10508  axpowndlem2  10510  axpowndlem3  10511  axpowndlem4  10512  axpownd  10513  axregndlem2  10515  axregnd  10516  axinfndlem1  10517  axinfnd  10518  axacndlem4  10522  axacndlem5  10523  axacnd  10524  axnulg  35239  axextdist  35967  axextbdist  35968  distel  35971  axtcond  36648  mh-setindnd  36707  wl-cbvalnaed  37845  wl-2sb6d  37871  wl-sbalnae  37875  wl-mo2df  37883  wl-mo2tf  37884  wl-eudf  37885  wl-eutf  37886  ax6e2ndeq  44974  ax6e2ndeqVD  45323