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

Theorem nfnae 2084
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 2082 . 2  |-  F/ z A. x  x  =  y
21nfn 1929 1  |-  F/ z  -.  A. x  x  =  y
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   A.wal 1403   F/wnf 1637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1634  df-nf 1638
This theorem is referenced by:  nfald2  2099  dvelimf  2102  sbequ6  2153  nfsb4t  2154  sbco2  2182  sbco3  2184  sb9  2193  2ax6elem  2217  sbal1  2228  sbal2  2229  axbnd  2379  nfabd2  2585  ralcom2  2971  dfid3  4738  nfriotad  6247  axextnd  8997  axrepndlem1  8998  axrepndlem2  8999  axrepnd  9000  axunndlem1  9001  axunnd  9002  axpowndlem2  9004  axpowndlem3  9005  axpowndlem4  9006  axpownd  9007  axregndlem2  9009  axregnd  9010  axregndOLD  9011  axinfndlem1  9012  axinfnd  9013  axacndlem4  9017  axacndlem5  9018  axacnd  9019  axextdist  30006  axext4dist  30007  distel  30010  wl-cbvalnaed  31337  wl-2sb6d  31360  wl-sbalnae  31364  wl-mo2dnae  31371  ax6e2ndeq  36336  ax6e2ndeqVD  36720
  Copyright terms: Public domain W3C validator