Theorem nfnae 2466

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

This proof depends on syntax axioms:  ¬ wn 3  ∀wal 1568  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-10 2180  ax-11 2197  ax-12 2216  ax-13 2404

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817

This theorem is used by:  nfald2  2477  dvelimf  2480  sbequ6  2498  2ax6elem  2502  nfsb4t  2531  sbco2  2543  sbco3  2545  sb9  2551  sbal1  2560  sbal2  2561  nfabd2  2949  ralcom2  3366  dfid3  5553  nfriotad  7408  axextnd  10700  axrepndlem1  10701  axrepndlem2  10702  axrepnd  10703  axunndlem1  10704  axunnd  10705  axpowndlem2  10707  axpowndlem3  10708  axpowndlem4  10709  axpownd  10710  axregndlem2  10712  axregnd  10713  axinfndlem1  10714  axinfnd  10715  axacndlem4  10719  axacndlem5  10720  axacnd  10721  axsepg2  35907  axsepg5  35911  axnulg  35912  axpowg2  35914  axpowg3  35915  axextdist  36738  axextbdist  36739  distel  36742  axtcond  37443  mh-setindnd  37502  wl-cbvalnaed  38655  wl-2sb6d  38681  wl-sbalnae  38685  wl-mo2df  38693  wl-mo2tf  38694  wl-eudf  38695  wl-eutf  38696  ax6e2ndeq  45731  ax6e2ndeqVD  46080