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

Theorem nfnae 2414
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
StepHypRef Expression
1 nfae 2412 . 2 𝑧𝑥 𝑥 = 𝑦
21nfn 1953 1 𝑧 ¬ ∀𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1650  wnf 1878
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879
This theorem is referenced by:  nfald2  2425  dvelimf  2428  sbequ6  2479  nfsb4t  2480  sbco2  2506  sbco3  2508  sb9  2517  2ax6elem  2541  sbal1  2552  sbal2  2553  axbnd  2742  nfabd2  2927  ralcom2  3251  dfid3  5188  nfriotad  6813  axextnd  9668  axrepndlem1  9669  axrepndlem2  9670  axrepnd  9671  axunndlem1  9672  axunnd  9673  axpowndlem2  9675  axpowndlem3  9676  axpowndlem4  9677  axpownd  9678  axregndlem2  9680  axregnd  9681  axinfndlem1  9682  axinfnd  9683  axacndlem4  9687  axacndlem5  9688  axacnd  9689  axextdist  32151  axext4dist  32152  distel  32155  wl-cbvalnaed  33747  wl-2sb6d  33769  wl-sbalnae  33773  wl-mo2df  33780  wl-mo2tf  33781  wl-eudf  33782  wl-eutf  33783  ax6e2ndeq  39440  ax6e2ndeqVD  39800
  Copyright terms: Public domain W3C validator