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

Theorem nfnae 2008
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 2006 . 2  |-  F/ z A. x  x  =  y
21nfn 1807 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  2014  dvelimh  2015  exdistrf  2028  nfald2  2029  equs5  2049  dvelimf  2050  sbequ6  2081  nfsb2  2107  nfsb4t  2129  dvelimdf  2131  sbco2  2135  sbco3  2137  sbcom  2138  sb9i  2143  sbal2  2184  nfeud2  2266  axbnd  2384  nfabd2  2558  ralcom2  2832  copsexg  4402  dfid3  4459  nfriotad  6517  axextnd  8422  axrepndlem1  8423  axrepndlem2  8424  axrepnd  8425  axunndlem1  8426  axunnd  8427  axpowndlem2  8429  axpowndlem3  8430  axpowndlem4  8431  axpownd  8432  axregndlem2  8434  axregnd  8435  axinfndlem1  8436  axinfnd  8437  axacndlem4  8441  axacndlem5  8442  axacnd  8443  axextdist  25370  axext4dist  25371  distel  25374  a9e2ndeq  28357  a9e2ndeqVD  28730
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946
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