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

Theorem nfnae 2058
Description: All variables are effectively bound in a distinct variable specifier. (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfnae

Proof of Theorem nfnae
StepHypRef Expression
1 nfae 2056 . 2
21nfn 1901 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  A.wal 1393  F/wnf 1616
This theorem is referenced by:  nfald2  2073  dvelimf  2076  sbequ6  2129  nfsb4t  2130  sbco2  2158  sbco3  2160  sb9  2169  2ax6elem  2193  sbal1  2204  sbal2  2205  axbnd  2434  nfabd2  2640  ralcom2  3022  copsexgOLD  4738  dfid3  4801  nfriotad  6265  axextnd  8987  axrepndlem1  8988  axrepndlem2  8989  axrepnd  8990  axunndlem1  8991  axunnd  8992  axpowndlem2  8994  axpowndlem2OLD  8995  axpowndlem3  8996  axpowndlem3OLD  8997  axpowndlem4  8998  axpownd  8999  axregndlem2  9001  axregnd  9002  axregndOLD  9003  axinfndlem1  9004  axinfnd  9005  axacndlem4  9009  axacndlem5  9010  axacnd  9011  axextdist  29232  axext4dist  29233  distel  29236  wl-cbvalnaed  29985  wl-2sb6d  30008  wl-sbalnae  30012  wl-mo2dnae  30019  ax6e2ndeq  33332  ax6e2ndeqVD  33709
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617
  Copyright terms: Public domain W3C validator