Theorem nfnae 2434

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

Syntax hints:  ¬ wn 3  ∀wal 1537  Ⅎwnf 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-10 2137  ax-11 2154  ax-12 2171  ax-13 2372

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787

This theorem is referenced by:  nfald2  2445  dvelimf  2448  sbequ6  2466  2ax6elem  2470  nfsb4t  2503  sbco2  2515  sbco3  2517  sb9  2523  sbal1  2533  sbal2  2534  nfabd2  2933  ralcom2  3290  dfid3  5492  nfriotad  7244  axextnd  10347  axrepndlem1  10348  axrepndlem2  10349  axrepnd  10350  axunndlem1  10351  axunnd  10352  axpowndlem2  10354  axpowndlem3  10355  axpowndlem4  10356  axpownd  10357  axregndlem2  10359  axregnd  10360  axinfndlem1  10361  axinfnd  10362  axacndlem4  10366  axacndlem5  10367  axacnd  10368  axextdist  33775  axextbdist  33776  distel  33779  wl-cbvalnaed  35691  wl-2sb6d  35713  wl-sbalnae  35717  wl-mo2df  35725  wl-mo2tf  35726  wl-eudf  35727  wl-eutf  35728  ax6e2ndeq  42179  ax6e2ndeqVD  42529