Theorem nfnae 2439

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

Syntax hints:  ¬ wn 3  ∀wal 1538  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-10 2142  ax-11 2158  ax-12 2178  ax-13 2377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfald2  2450  dvelimf  2453  sbequ6  2471  2ax6elem  2475  nfsb4t  2504  sbco2  2516  sbco3  2518  sb9  2524  sbal1  2533  sbal2  2534  nfabd2  2923  ralcom2  3361  dfid3  5556  nfriotad  7378  axextnd  10610  axrepndlem1  10611  axrepndlem2  10612  axrepnd  10613  axunndlem1  10614  axunnd  10615  axpowndlem2  10617  axpowndlem3  10618  axpowndlem4  10619  axpownd  10620  axregndlem2  10622  axregnd  10623  axinfndlem1  10624  axinfnd  10625  axacndlem4  10629  axacndlem5  10630  axacnd  10631  axnulg  35128  axextdist  35822  axextbdist  35823  distel  35826  wl-cbvalnaed  37555  wl-2sb6d  37581  wl-sbalnae  37585  wl-mo2df  37593  wl-mo2tf  37594  wl-eudf  37595  wl-eutf  37596  ax6e2ndeq  44551  ax6e2ndeqVD  44900