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

Theorem nfnae 2015
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 2013 . 2  |-  F/ z A. x  x  =  y
21nfn 1837 1  |-  F/ z  -.  A. x  x  =  y
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   A.wal 1368   F/wnf 1590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591
This theorem is referenced by:  nfald2  2030  dvelimf  2033  sbequ6  2086  nfsb4t  2087  sbco2OLD  2119  sbco3  2121  sbco3OLD  2122  sb9  2133  sb9iOLD  2135  2ax6elem  2164  sbal1  2178  sbal2  2180  sbal2OLD  2191  nfeud2OLD  2287  axbnd  2429  nfabd2  2633  ralcom2  2983  copsexgOLD  4677  dfid3  4737  nfriotad  6161  axextnd  8858  axrepndlem1  8859  axrepndlem2  8860  axrepnd  8861  axunndlem1  8862  axunnd  8863  axpowndlem2  8865  axpowndlem2OLD  8866  axpowndlem3  8867  axpowndlem3OLD  8868  axpowndlem4  8869  axpownd  8870  axregndlem2  8872  axregnd  8873  axregndOLD  8874  axinfndlem1  8875  axinfnd  8876  axacndlem4  8880  axacndlem5  8881  axacnd  8882  axextdist  27749  axext4dist  27750  distel  27753  wl-2sb6d  28524  wl-sbalnae  28528  ax6e2ndeq  31570  ax6e2ndeqVD  31947
  Copyright terms: Public domain W3C validator