Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nfnae | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
nfnae | ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfae 2433 | . 2 ⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦 | |
2 | 1 | nfn 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 |