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

Theorem nfnae 1909
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 1907 . 2  |-  F/ z A. x  x  =  y
21nfn 1777 1  |-  F/ z  -.  A. x  x  =  y
Colors of variables: wff set class
Syntax hints:   -. wn 3   A.wal 1530   F/wnf 1534
This theorem is referenced by:  nfeqf  1911  exdistrf  1924  nfald2  1925  equs5  1949  dvelimf  1950  sbequ6  1985  nfsb2  2011  nfsb4t  2033  dvelimdf  2035  sbco2  2039  sbco3  2041  sbcom  2042  sb9i  2047  sbal2  2086  nfeud2  2168  nfabd2  2450  ralcom2  2717  copsexg  4268  dfid3  4326  nfriotad  6329  axextnd  8229  axrepndlem1  8230  axrepndlem2  8231  axrepnd  8232  axunndlem1  8233  axunnd  8234  axpowndlem2  8236  axpowndlem3  8237  axpowndlem4  8238  axpownd  8239  axregndlem2  8241  axregnd  8242  axinfndlem1  8243  axinfnd  8244  axacndlem4  8248  axacndlem5  8249  axacnd  8250  axextdist  24227  axext4dist  24228  distel  24231  a9e2ndeq  28624  a9e2ndeqVD  29001  a12lem1  29752
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535
  Copyright terms: Public domain W3C validator