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 2183  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  2921  ralcom2  3346  dfid3  5521  nfriotad  7326  axextnd  10504  axrepndlem1  10505  axrepndlem2  10506  axrepnd  10507  axunndlem1  10508  axunnd  10509  axpowndlem2  10511  axpowndlem3  10512  axpowndlem4  10513  axpownd  10514  axregndlem2  10516  axregnd  10517  axinfndlem1  10518  axinfnd  10519  axacndlem4  10523  axacndlem5  10524  axacnd  10525  axnulg  35243  axextdist  35970  axextbdist  35971  distel  35974  wl-cbvalnaed  37706  wl-2sb6d  37732  wl-sbalnae  37736  wl-mo2df  37744  wl-mo2tf  37745  wl-eudf  37746  wl-eutf  37747  ax6e2ndeq  44837  ax6e2ndeqVD  45186