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

Theorem nfnae 2045
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 2043 . 2  |-  F/ z A. x  x  =  y
21nfn 1812 1  |-  F/ z  -.  A. x  x  =  y
Colors of variables: wff set class
Syntax hints:   -. wn 3   A.wal 1550   F/wnf 1554
This theorem is referenced by:  nfeqfOLD  2055  nfald2  2065  exdistrfOLD  2068  dvelimf  2069  dvelimfOLD  2070  equs5  2090  nfsb2  2097  sbequ6  2126  nfsb4t  2128  nfsb4tOLD  2129  dvelimdfOLD  2158  sbco2  2162  sbco3  2164  sbcom  2165  sbcomOLD  2166  sb9i  2171  sbal2  2212  nfeud2  2294  axbnd  2417  nfabd2  2591  ralcom2  2873  copsexg  4443  dfid3  4500  nfriotad  6559  axextnd  8467  axrepndlem1  8468  axrepndlem2  8469  axrepnd  8470  axunndlem1  8471  axunnd  8472  axpowndlem2  8474  axpowndlem3  8475  axpowndlem4  8476  axpownd  8477  axregndlem2  8479  axregnd  8480  axinfndlem1  8481  axinfnd  8482  axacndlem4  8486  axacndlem5  8487  axacnd  8488  axextdist  25428  axext4dist  25429  distel  25432  a9e2ndeq  28647  a9e2ndeqVD  29022
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555
  Copyright terms: Public domain W3C validator