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

Theorem nfnae 1896
Description: All variables are effectively bound in an 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 1894 . 2  |-  F/ z A. x  x  =  y
21nfn 1765 1  |-  F/ z  -.  A. x  x  =  y
Colors of variables: wff set class
Syntax hints:   -. wn 3   A.wal 1527   F/wnf 1531
This theorem is referenced by:  nfeqf  1898  exdistrf  1911  nfald2  1912  equs5  1936  dvelimf  1937  sbequ6  1972  nfsb2  1998  nfsb4t  2020  dvelimdf  2022  sbco2  2026  sbco3  2028  sbcom  2029  sb9i  2034  sbal2  2073  nfeud2  2155  nfabd2  2437  ralcom2  2704  copsexg  4252  dfid3  4310  nfriotad  6313  axextnd  8213  axrepndlem1  8214  axrepndlem2  8215  axrepnd  8216  axunndlem1  8217  axunnd  8218  axpowndlem2  8220  axpowndlem3  8221  axpowndlem4  8222  axpownd  8223  axregndlem2  8225  axregnd  8226  axinfndlem1  8227  axinfnd  8228  axacndlem4  8232  axacndlem5  8233  axacnd  8234  axextdist  24156  axext4dist  24157  distel  24160  a9e2ndeq  28325  a9e2ndeqVD  28685  a12lem1  29130
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532
  Copyright terms: Public domain W3C validator