Theorem nfnae 2465

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

This proof depends on syntax axioms:  ¬ wn 3  ∀wal 1567  Ⅎwnf 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-10 2175  ax-11 2191  ax-12 2212  ax-13 2403

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1572  df-ex 1809  df-nf 1813

This theorem is used by:  nfald2  2476  dvelimf  2479  sbequ6  2497  2ax6elem  2501  nfsb4t  2530  sbco2  2542  sbco3  2544  sb9  2550  sbal1  2559  sbal2  2560  nfabd2  2947  ralcom2  3365  dfid3  5558  nfriotad  7380  axextnd  10582  axrepndlem1  10583  axrepndlem2  10584  axrepnd  10585  axunndlem1  10586  axunnd  10587  axpowndlem2  10589  axpowndlem3  10590  axpowndlem4  10591  axpownd  10592  axregndlem2  10594  axregnd  10595  axinfndlem1  10596  axinfnd  10597  axacndlem4  10601  axacndlem5  10602  axacnd  10603  axsepg2  35561  axsepg5  35565  axnulg  35566  axpowg2  35568  axpowg3  35569  axextdist  36297  axextbdist  36298  distel  36301  axtcond  37017  mh-setindnd  37076  wl-cbvalnaed  38215  wl-2sb6d  38241  wl-sbalnae  38245  wl-mo2df  38253  wl-mo2tf  38254  wl-eudf  38255  wl-eutf  38256  ax6e2ndeq  45296  ax6e2ndeqVD  45645