Theorem nfnae 2306

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 2304	. 2 ⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦
2	1	nfn 1768	1 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦

Syntax hints:  ¬ wn 3  ∀wal 1473  Ⅎwnf 1699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701

This theorem is referenced by:  nfald2  2319  dvelimf  2322  sbequ6  2376  nfsb4t  2377  sbco2  2403  sbco3  2405  sb9  2414  2ax6elem  2437  sbal1  2448  sbal2  2449  axbnd  2589  nfabd2  2770  ralcom2  3083  dfid3  4954  nfriotad  6519  axextnd  9292  axrepndlem1  9293  axrepndlem2  9294  axrepnd  9295  axunndlem1  9296  axunnd  9297  axpowndlem2  9299  axpowndlem3  9300  axpowndlem4  9301  axpownd  9302  axregndlem2  9304  axregnd  9305  axinfndlem1  9306  axinfnd  9307  axacndlem4  9311  axacndlem5  9312  axacnd  9313  axextdist  30949  axext4dist  30950  distel  30953  bj-axc14nf  32031  wl-cbvalnaed  32498  wl-2sb6d  32520  wl-sbalnae  32524  wl-mo2df  32531  wl-mo2tf  32532  wl-eudf  32533  wl-eutf  32534  wl-euequ1f  32535  ax6e2ndeq  37796  ax6e2ndeqVD  38167