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 2185 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 1889	1 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-10 2177  ax-11 2193  ax-12 2212  ax-13 2401

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816

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  5548  nfriotad  7388  axextnd  10676  axrepndlem1  10677  axrepndlem2  10678  axrepnd  10679  axunndlem1  10680  axunnd  10681  axpowndlem2  10683  axpowndlem3  10684  axpowndlem4  10685  axpownd  10686  axregndlem2  10688  axregnd  10689  axinfndlem1  10690  axinfnd  10691  axacndlem4  10695  axacndlem5  10696  axacnd  10697  axsepg2  35808  axsepg5  35812  axnulg  35813  axpowg2  35815  axpowg3  35816  axextdist  36561  axextbdist  36562  distel  36565  axtcond  37266  mh-setindnd  37325  wl-cbvalnaed  38465  wl-2sb6d  38491  wl-sbalnae  38495  wl-mo2df  38503  wl-mo2tf  38504  wl-eudf  38505  wl-eutf  38506  ax6e2ndeq  45542  ax6e2ndeqVD  45891