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

Theorem nfnae 2026
Description: All variables are effectively bound in a distinct variable specifier. (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfnae  |-  F/ z  -.  A. x  x  =  y

Proof of Theorem nfnae
StepHypRef Expression
1 nfae 2024 . 2  |-  F/ z A. x  x  =  y
21nfn 1844 1  |-  F/ z  -.  A. x  x  =  y
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   A.wal 1372   F/wnf 1594
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-nf 1595
This theorem is referenced by:  nfald2  2041  dvelimf  2044  sbequ6  2097  nfsb4t  2098  sbco2OLD  2130  sbco3  2132  sbco3OLD  2133  sb9  2144  sb9iOLD  2146  2ax6elem  2174  sbal1  2188  sbal2  2190  sbal2OLD  2201  nfeud2OLD  2297  axbnd  2439  nfabd2  2645  ralcom2  3021  copsexgOLD  4728  dfid3  4791  nfriotad  6246  axextnd  8957  axrepndlem1  8958  axrepndlem2  8959  axrepnd  8960  axunndlem1  8961  axunnd  8962  axpowndlem2  8964  axpowndlem2OLD  8965  axpowndlem3  8966  axpowndlem3OLD  8967  axpowndlem4  8968  axpownd  8969  axregndlem2  8971  axregnd  8972  axregndOLD  8973  axinfndlem1  8974  axinfnd  8975  axacndlem4  8979  axacndlem5  8980  axacnd  8981  axextdist  28797  axext4dist  28798  distel  28801  wl-2sb6d  29573  wl-sbalnae  29577  ax6e2ndeq  32289  ax6e2ndeqVD  32666
  Copyright terms: Public domain W3C validator