Theorem nfnae 2425

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

Syntax hints:  ¬ wn 3  ∀wal 1531  Ⅎwnf 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-10 2129  ax-11 2146  ax-12 2163  ax-13 2363

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1536  df-ex 1774  df-nf 1778

This theorem is referenced by:  nfald2  2436  dvelimf  2439  sbequ6  2457  2ax6elem  2461  nfsb4t  2490  sbco2  2502  sbco3  2504  sb9  2510  sbal1  2519  sbal2  2520  nfabd2  2921  ralcom2  3365  dfid3  5568  nfriotad  7370  axextnd  10583  axrepndlem1  10584  axrepndlem2  10585  axrepnd  10586  axunndlem1  10587  axunnd  10588  axpowndlem2  10590  axpowndlem3  10591  axpowndlem4  10592  axpownd  10593  axregndlem2  10595  axregnd  10596  axinfndlem1  10597  axinfnd  10598  axacndlem4  10602  axacndlem5  10603  axacnd  10604  axextdist  35267  axextbdist  35268  distel  35271  wl-cbvalnaed  36892  wl-2sb6d  36917  wl-sbalnae  36921  wl-mo2df  36929  wl-mo2tf  36930  wl-eudf  36931  wl-eutf  36932  ax6e2ndeq  43834  ax6e2ndeqVD  44184