Theorem nfnae 2432

Description: All variables are effectively bound in a distinct variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2370. 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 2431	. 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 2370

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  2443  dvelimf  2446  sbequ6  2464  2ax6elem  2468  nfsb4t  2497  sbco2  2509  sbco3  2511  sb9  2517  sbal1  2526  sbal2  2527  nfabd2  2915  ralcom2  3351  dfid3  5536  nfriotad  7355  axextnd  10544  axrepndlem1  10545  axrepndlem2  10546  axrepnd  10547  axunndlem1  10548  axunnd  10549  axpowndlem2  10551  axpowndlem3  10552  axpowndlem4  10553  axpownd  10554  axregndlem2  10556  axregnd  10557  axinfndlem1  10558  axinfnd  10559  axacndlem4  10563  axacndlem5  10564  axacnd  10565  axnulg  35082  axextdist  35787  axextbdist  35788  distel  35791  wl-cbvalnaed  37520  wl-2sb6d  37546  wl-sbalnae  37550  wl-mo2df  37558  wl-mo2tf  37559  wl-eudf  37560  wl-eutf  37561  ax6e2ndeq  44549  ax6e2ndeqVD  44898