Theorem nfnae 2452

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

Syntax hints:  ¬ wn 3  ∀wal 1531  Ⅎ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 1907  ax-6 1966  ax-7 2011  ax-10 2141  ax-11 2156  ax-12 2172  ax-13 2386

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781

This theorem is referenced by:  nfald2  2463  dvelimf  2466  sbequ6  2485  2ax6elem  2489  nfsb4t  2535  sbco2  2549  sbco3  2551  sb9  2557  sbal1  2568  sbal2  2569  sbal2OLD  2570  nfsb4tALT  2600  sbco2ALT  2611  axbndOLD  2792  nfabd2  3002  nfabd2OLD  3003  ralcom2  3364  dfid3  5457  nfriotad  7119  axextnd  10007  axrepndlem1  10008  axrepndlem2  10009  axrepnd  10010  axunndlem1  10011  axunnd  10012  axpowndlem2  10014  axpowndlem3  10015  axpowndlem4  10016  axpownd  10017  axregndlem2  10019  axregnd  10020  axinfndlem1  10021  axinfnd  10022  axacndlem4  10026  axacndlem5  10027  axacnd  10028  axextdist  33039  axextbdist  33040  distel  33043  wl-cbvalnaed  34766  wl-2sb6d  34788  wl-sbalnae  34792  wl-mo2df  34800  wl-mo2tf  34801  wl-eudf  34802  wl-eutf  34803  ax6e2ndeq  40886  ax6e2ndeqVD  41236