Theorem nfnae 2463

Description: All variables are effectively bound in a distinct variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2401. Use the weaker nfnaew 2186 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 2462	. 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 1943  ax-6 2000  ax-7 2041  ax-10 2178  ax-11 2194  ax-12 2213  ax-13 2401

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  2474  dvelimf  2477  sbequ6  2495  2ax6elem  2499  nfsb4t  2528  sbco2  2540  sbco3  2542  sb9  2548  sbal1  2557  sbal2  2558  nfabd2  2945  ralcom2  3362  dfid3  5546  nfriotad  7377  axextnd  10633  axrepndlem1  10634  axrepndlem2  10635  axrepnd  10636  axunndlem1  10637  axunnd  10638  axpowndlem2  10640  axpowndlem3  10641  axpowndlem4  10642  axpownd  10643  axregndlem2  10645  axregnd  10646  axinfndlem1  10647  axinfnd  10648  axacndlem4  10652  axacndlem5  10653  axacnd  10654  axsepg2  35727  axsepg5  35731  axnulg  35732  axpowg2  35734  axpowg3  35735  axextdist  36477  axextbdist  36478  distel  36481  axtcond  37182  mh-setindnd  37241  wl-cbvalnaed  38378  wl-2sb6d  38404  wl-sbalnae  38408  wl-mo2df  38416  wl-mo2tf  38417  wl-eudf  38418  wl-eutf  38419  ax6e2ndeq  45480  ax6e2ndeqVD  45829