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 2152 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 1858	1 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦

Syntax hints:  ¬ wn 3  ∀wal 1539  Ⅎwnf 1784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-10 2144  ax-11 2160  ax-12 2180  ax-13 2372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785

This theorem is referenced by:  nfald2  2445  dvelimf  2448  sbequ6  2466  2ax6elem  2470  nfsb4t  2499  sbco2  2511  sbco3  2513  sb9  2519  sbal1  2528  sbal2  2529  nfabd2  2918  ralcom2  3343  dfid3  5512  nfriotad  7314  axextnd  10482  axrepndlem1  10483  axrepndlem2  10484  axrepnd  10485  axunndlem1  10486  axunnd  10487  axpowndlem2  10489  axpowndlem3  10490  axpowndlem4  10491  axpownd  10492  axregndlem2  10494  axregnd  10495  axinfndlem1  10496  axinfnd  10497  axacndlem4  10501  axacndlem5  10502  axacnd  10503  axnulg  35119  axextdist  35841  axextbdist  35842  distel  35845  wl-cbvalnaed  37576  wl-2sb6d  37602  wl-sbalnae  37606  wl-mo2df  37614  wl-mo2tf  37615  wl-eudf  37616  wl-eutf  37617  ax6e2ndeq  44651  ax6e2ndeqVD  45000