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

Theorem nfnae 2059
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 2057 . 2  |-  F/ z A. x  x  =  y
21nfn 1902 1  |-  F/ z  -.  A. x  x  =  y
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   A.wal 1393   F/wnf 1617
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1614  df-nf 1618
This theorem is referenced by:  nfald2  2074  dvelimf  2077  sbequ6  2130  nfsb4t  2131  sbco2  2159  sbco3  2161  sb9  2170  2ax6elem  2194  sbal1  2205  sbal2  2206  axbnd  2434  nfabd2  2640  ralcom2  3022  copsexgOLD  4742  dfid3  4805  nfriotad  6266  axextnd  8983  axrepndlem1  8984  axrepndlem2  8985  axrepnd  8986  axunndlem1  8987  axunnd  8988  axpowndlem2  8990  axpowndlem2OLD  8991  axpowndlem3  8992  axpowndlem3OLD  8993  axpowndlem4  8994  axpownd  8995  axregndlem2  8997  axregnd  8998  axregndOLD  8999  axinfndlem1  9000  axinfnd  9001  axacndlem4  9005  axacndlem5  9006  axacnd  9007  axextdist  29449  axext4dist  29450  distel  29453  wl-cbvalnaed  30190  wl-2sb6d  30213  wl-sbalnae  30217  wl-mo2dnae  30224  ax6e2ndeq  33475  ax6e2ndeqVD  33852
  Copyright terms: Public domain W3C validator