Theorem nfnae 2444

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

Syntax hints:  ¬ wn 3  ∀wal 1546  Ⅎwnf 1791

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-10 2154  ax-11 2170  ax-12 2191  ax-13 2382

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-tru 1551  df-ex 1788  df-nf 1792

This theorem is referenced by:  nfald2  2455  dvelimf  2458  sbequ6  2476  2ax6elem  2480  nfsb4t  2509  sbco2  2521  sbco3  2523  sb9  2529  sbal1  2538  sbal2  2539  nfabd2  2926  ralcom2  3343  dfid3  5518  nfriotad  7327  axextnd  10510  axrepndlem1  10511  axrepndlem2  10512  axrepnd  10513  axunndlem1  10514  axunnd  10515  axpowndlem2  10517  axpowndlem3  10518  axpowndlem4  10519  axpownd  10520  axregndlem2  10522  axregnd  10523  axinfndlem1  10524  axinfnd  10525  axacndlem4  10529  axacndlem5  10530  axacnd  10531  axsepg2  35334  axsepg5  35338  axnulg  35339  axpowg2  35341  axpowg3  35342  axextdist  36038  axextbdist  36039  distel  36042  axtcond  36719  mh-setindnd  36778  wl-cbvalnaed  37916  wl-2sb6d  37942  wl-sbalnae  37946  wl-mo2df  37954  wl-mo2tf  37955  wl-eudf  37956  wl-eutf  37957  ax6e2ndeq  45016  ax6e2ndeqVD  45365