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

Theorem nfnae 2434
Description: All variables are effectively bound in a distinct variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker nfnaew 2145 when possible. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.)
Assertion
Ref Expression
nfnae 𝑧 ¬ ∀𝑥 𝑥 = 𝑦

Proof of Theorem nfnae
StepHypRef Expression
1 nfae 2433 . 2 𝑧𝑥 𝑥 = 𝑦
21nfn 1860 1 𝑧 ¬ ∀𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1537  wnf 1786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-10 2137  ax-11 2154  ax-12 2171  ax-13 2372
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787
This theorem is referenced by:  nfald2  2445  dvelimf  2448  sbequ6  2466  2ax6elem  2470  nfsb4t  2503  sbco2  2515  sbco3  2517  sb9  2523  sbal1  2533  sbal2  2534  nfabd2  2933  ralcom2  3290  dfid3  5492  nfriotad  7244  axextnd  10347  axrepndlem1  10348  axrepndlem2  10349  axrepnd  10350  axunndlem1  10351  axunnd  10352  axpowndlem2  10354  axpowndlem3  10355  axpowndlem4  10356  axpownd  10357  axregndlem2  10359  axregnd  10360  axinfndlem1  10361  axinfnd  10362  axacndlem4  10366  axacndlem5  10367  axacnd  10368  axextdist  33775  axextbdist  33776  distel  33779  wl-cbvalnaed  35691  wl-2sb6d  35713  wl-sbalnae  35717  wl-mo2df  35725  wl-mo2tf  35726  wl-eudf  35727  wl-eutf  35728  ax6e2ndeq  42179  ax6e2ndeqVD  42529
  Copyright terms: Public domain W3C validator