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

Theorem nfnae 1987
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 1985 . 2  |-  F/ z A. x  x  =  y
21nfn 1801 1  |-  F/ z  -.  A. x  x  =  y
Colors of variables: wff set class
Syntax hints:   -. wn 3   A.wal 1546   F/wnf 1550
This theorem is referenced by:  nfeqf  1989  exdistrf  1997  nfald2  1998  equs5  2022  dvelimf  2023  sbequ6  2058  nfsb2  2084  nfsb4t  2106  dvelimdf  2108  sbco2  2112  sbco3  2114  sbcom  2115  sb9i  2120  sbal2  2161  nfeud2  2243  nfabd2  2534  ralcom2  2808  copsexg  4376  dfid3  4433  nfriotad  6487  axextnd  8392  axrepndlem1  8393  axrepndlem2  8394  axrepnd  8395  axunndlem1  8396  axunnd  8397  axpowndlem2  8399  axpowndlem3  8400  axpowndlem4  8401  axpownd  8402  axregndlem2  8404  axregnd  8405  axinfndlem1  8406  axinfnd  8407  axacndlem4  8411  axacndlem5  8412  axacnd  8413  axextdist  25173  axext4dist  25174  distel  25177  a9e2ndeq  27982  a9e2ndeqVD  28355  a12lem1  29106
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator