Theorem nfnae 2448

Description: All variables are effectively bound in a distinct variable specifier. (Contributed by Mario Carneiro, 11-Aug-2016.)

Assertion

Ref	Expression
nfnae	⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦

Proof of Theorem nfnae

Step	Hyp	Ref	Expression
1		nfae 2446	. 2 ⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦
2	1	nfn 1921	1 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦

Syntax hints:  ¬ wn 3  ∀wal 1618  Ⅎwnf 1845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1623  df-ex 1842  df-nf 1847

This theorem is referenced by:  nfald2  2459  dvelimf  2462  sbequ6  2513  nfsb4t  2514  sbco2  2540  sbco3  2542  sb9  2551  2ax6elem  2574  sbal1  2585  sbal2  2586  axbnd  2727  nfabd2  2910  ralcom2  3230  dfid3  5163  nfriotad  6770  axextnd  9576  axrepndlem1  9577  axrepndlem2  9578  axrepnd  9579  axunndlem1  9580  axunnd  9581  axpowndlem2  9583  axpowndlem3  9584  axpowndlem4  9585  axpownd  9586  axregndlem2  9588  axregnd  9589  axinfndlem1  9590  axinfnd  9591  axacndlem4  9595  axacndlem5  9596  axacnd  9597  axextdist  31981  axext4dist  31982  distel  31985  bj-axc14nf  33115  wl-cbvalnaed  33601  wl-2sb6d  33623  wl-sbalnae  33627  wl-mo2df  33634  wl-mo2tf  33635  wl-eudf  33636  wl-eutf  33637  wl-euequ1f  33638  ax6e2ndeq  39246  ax6e2ndeqVD  39613