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

Theorem nfnae 2316
 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 2314 . 2 𝑧𝑥 𝑥 = 𝑦
21nfn 1782 1 𝑧 ¬ ∀𝑥 𝑥 = 𝑦
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3  ∀wal 1479  Ⅎwnf 1706 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708 This theorem is referenced by:  nfald2  2329  dvelimf  2332  sbequ6  2386  nfsb4t  2387  sbco2  2413  sbco3  2415  sb9  2424  2ax6elem  2447  sbal1  2458  sbal2  2459  axbnd  2599  nfabd2  2781  ralcom2  3099  dfid3  5015  nfriotad  6604  axextnd  9398  axrepndlem1  9399  axrepndlem2  9400  axrepnd  9401  axunndlem1  9402  axunnd  9403  axpowndlem2  9405  axpowndlem3  9406  axpowndlem4  9407  axpownd  9408  axregndlem2  9410  axregnd  9411  axinfndlem1  9412  axinfnd  9413  axacndlem4  9417  axacndlem5  9418  axacnd  9419  axextdist  31679  axext4dist  31680  distel  31683  bj-axc14nf  32813  wl-cbvalnaed  33290  wl-2sb6d  33312  wl-sbalnae  33316  wl-mo2df  33323  wl-mo2tf  33324  wl-eudf  33325  wl-eutf  33326  wl-euequ1f  33327  ax6e2ndeq  38595  ax6e2ndeqVD  38965
 Copyright terms: Public domain W3C validator