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

Theorem nfnae 2167
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 2165 . 2  |-  F/ z A. x  x  =  y
21nfn 2003 1  |-  F/ z  -.  A. x  x  =  y
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   A.wal 1450   F/wnf 1675
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104
This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672  df-nf 1676
This theorem is referenced by:  nfald2  2180  dvelimf  2183  sbequ6  2237  nfsb4t  2238  sbco2  2264  sbco3  2266  sb9  2275  2ax6elem  2298  sbal1  2309  sbal2  2310  axbnd  2450  nfabd2  2631  ralcom2  2941  dfid3  4755  nfriotad  6278  axextnd  9034  axrepndlem1  9035  axrepndlem2  9036  axrepnd  9037  axunndlem1  9038  axunnd  9039  axpowndlem2  9041  axpowndlem3  9042  axpowndlem4  9043  axpownd  9044  axregndlem2  9046  axregnd  9047  axinfndlem1  9048  axinfnd  9049  axacndlem4  9053  axacndlem5  9054  axacnd  9055  axextdist  30517  axext4dist  30518  distel  30521  wl-cbvalnaed  31935  wl-2sb6d  31958  wl-sbalnae  31962  wl-mo2df  31969  wl-mo2tf  31970  wl-eudf  31971  wl-eutf  31972  wl-euequ1f  31973  ax6e2ndeq  36996  ax6e2ndeqVD  37369
  Copyright terms: Public domain W3C validator