Theorem nfnae 2467

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

Syntax hints:  ¬ wn 3  ∀wal 1560  Ⅎwnf 1805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-10 2177  ax-11 2193  ax-12 2214  ax-13 2405

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1565  df-ex 1802  df-nf 1806

This theorem is referenced by:  nfald2  2478  dvelimf  2481  sbequ6  2499  2ax6elem  2503  nfsb4t  2532  sbco2  2544  sbco3  2546  sb9  2552  sbal1  2561  sbal2  2562  nfabd2  2949  ralcom2  3366  dfid3  5547  nfriotad  7366  axextnd  10551  axrepndlem1  10552  axrepndlem2  10553  axrepnd  10554  axunndlem1  10555  axunnd  10556  axpowndlem2  10558  axpowndlem3  10559  axpowndlem4  10560  axpownd  10561  axregndlem2  10563  axregnd  10564  axinfndlem1  10565  axinfnd  10566  axacndlem4  10570  axacndlem5  10571  axacnd  10572  axsepg2  35440  axsepg5  35444  axnulg  35445  axpowg2  35447  axpowg3  35448  axextdist  36152  axextbdist  36153  distel  36156  axtcond  36843  mh-setindnd  36902  wl-cbvalnaed  38040  wl-2sb6d  38066  wl-sbalnae  38070  wl-mo2df  38078  wl-mo2tf  38079  wl-eudf  38080  wl-eutf  38081  ax6e2ndeq  45140  ax6e2ndeqVD  45489