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 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 2464	. 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 2215  ax-13 2403

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  2476  dvelimf  2479  sbequ6  2497  2ax6elem  2501  nfsb4t  2530  sbco2  2542  sbco3  2544  sb9  2550  sbal1  2559  sbal2  2560  nfabd2  2947  ralcom2  3364  dfid3  5557  nfriotad  7384  axextnd  10603  axrepndlem1  10604  axrepndlem2  10605  axrepnd  10606  axunndlem1  10607  axunnd  10608  axpowndlem2  10610  axpowndlem3  10611  axpowndlem4  10612  axpownd  10613  axregndlem2  10615  axregnd  10616  axinfndlem1  10617  axinfnd  10618  axacndlem4  10622  axacndlem5  10623  axacnd  10624  axsepg2  35653  axsepg5  35657  axnulg  35658  axpowg2  35660  axpowg3  35661  axextdist  36363  axextbdist  36364  distel  36367  axtcond  37084  mh-setindnd  37143  wl-cbvalnaed  38282  wl-2sb6d  38308  wl-sbalnae  38312  wl-mo2df  38320  wl-mo2tf  38321  wl-eudf  38322  wl-eutf  38323  ax6e2ndeq  45369  ax6e2ndeqVD  45718