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

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

Proof of Theorem nfnae
StepHypRef Expression
1 nfae 2447 . 2 𝑧𝑥 𝑥 = 𝑦
21nfn 1848 1 𝑧 ¬ ∀𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1526  wnf 1775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-10 2136  ax-11 2151  ax-12 2167  ax-13 2381
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776
This theorem is referenced by:  nfald2  2459  dvelimf  2462  sbequ6  2481  2ax6elem  2485  nfsb4t  2532  sbco2  2546  sbco3  2548  sb9  2554  sbal1  2565  sbal2  2566  sbal2OLD  2567  nfsb4tALT  2597  sbco2ALT  2608  axbndOLD  2789  nfabd2  2999  nfabd2OLD  3000  ralcom2  3361  dfid3  5455  nfriotad  7114  axextnd  10001  axrepndlem1  10002  axrepndlem2  10003  axrepnd  10004  axunndlem1  10005  axunnd  10006  axpowndlem2  10008  axpowndlem3  10009  axpowndlem4  10010  axpownd  10011  axregndlem2  10013  axregnd  10014  axinfndlem1  10015  axinfnd  10016  axacndlem4  10020  axacndlem5  10021  axacnd  10022  axextdist  32941  axextbdist  32942  distel  32945  wl-cbvalnaed  34653  wl-2sb6d  34675  wl-sbalnae  34679  wl-mo2df  34687  wl-mo2tf  34688  wl-eudf  34689  wl-eutf  34690  ax6e2ndeq  40770  ax6e2ndeqVD  41120
  Copyright terms: Public domain W3C validator