MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfnae Structured version   Visualization version   GIF version

Theorem nfnae 2453
Description: All variables are effectively bound in a distinct variable specifier. See also nfnaew 2146. (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfnae 𝑧 ¬ ∀𝑥 𝑥 = 𝑦

Proof of Theorem nfnae
StepHypRef Expression
1 nfae 2452 . 2 𝑧𝑥 𝑥 = 𝑦
21nfn 1850 1 𝑧 ¬ ∀𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1528  wnf 1777
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-10 2138  ax-11 2153  ax-12 2169  ax-13 2385
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778
This theorem is referenced by:  nfald2  2464  dvelimf  2467  sbequ6  2486  2ax6elem  2490  nfsb4t  2537  sbco2  2551  sbco3  2553  sb9  2559  sbal1  2569  sbal2  2570  sbal2OLD  2571  nfsb4tALT  2601  sbco2ALT  2612  axbndOLD  2796  nfabd2  3006  nfabd2OLD  3007  ralcom2  3368  dfid3  5460  nfriotad  7120  axextnd  10005  axrepndlem1  10006  axrepndlem2  10007  axrepnd  10008  axunndlem1  10009  axunnd  10010  axpowndlem2  10012  axpowndlem3  10013  axpowndlem4  10014  axpownd  10015  axregndlem2  10017  axregnd  10018  axinfndlem1  10019  axinfnd  10020  axacndlem4  10024  axacndlem5  10025  axacnd  10026  axextdist  32931  axextbdist  32932  distel  32935  wl-cbvalnaed  34643  wl-2sb6d  34664  wl-sbalnae  34668  wl-mo2df  34676  wl-mo2tf  34677  wl-eudf  34678  wl-eutf  34679  ax6e2ndeq  40761  ax6e2ndeqVD  41111
  Copyright terms: Public domain W3C validator