Theorem nfnae 2437

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

Syntax hints:  ¬ wn 3  ∀wal 1535  Ⅎwnf 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-10 2139  ax-11 2155  ax-12 2175  ax-13 2375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-nf 1781

This theorem is referenced by:  nfald2  2448  dvelimf  2451  sbequ6  2469  2ax6elem  2473  nfsb4t  2502  sbco2  2514  sbco3  2516  sb9  2522  sbal1  2531  sbal2  2532  nfabd2  2927  ralcom2  3375  dfid3  5586  nfriotad  7399  axextnd  10629  axrepndlem1  10630  axrepndlem2  10631  axrepnd  10632  axunndlem1  10633  axunnd  10634  axpowndlem2  10636  axpowndlem3  10637  axpowndlem4  10638  axpownd  10639  axregndlem2  10641  axregnd  10642  axinfndlem1  10643  axinfnd  10644  axacndlem4  10648  axacndlem5  10649  axacnd  10650  axnulg  35085  axextdist  35781  axextbdist  35782  distel  35785  wl-cbvalnaed  37513  wl-2sb6d  37539  wl-sbalnae  37543  wl-mo2df  37551  wl-mo2tf  37552  wl-eudf  37553  wl-eutf  37554  ax6e2ndeq  44557  ax6e2ndeqVD  44907