![]() |
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 2146 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 1861 | 1 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∀wal 1540 Ⅎ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 1914 ax-6 1972 ax-7 2012 ax-10 2138 ax-11 2155 ax-12 2172 ax-13 2372 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-nf 1787 |
This theorem is referenced by: nfald2 2445 dvelimf 2448 sbequ6 2466 2ax6elem 2470 nfsb4t 2499 sbco2 2511 sbco3 2513 sb9 2519 sbal1 2528 sbal2 2529 nfabd2 2930 ralcom2 3374 dfid3 5578 nfriotad 7377 axextnd 10586 axrepndlem1 10587 axrepndlem2 10588 axrepnd 10589 axunndlem1 10590 axunnd 10591 axpowndlem2 10593 axpowndlem3 10594 axpowndlem4 10595 axpownd 10596 axregndlem2 10598 axregnd 10599 axinfndlem1 10600 axinfnd 10601 axacndlem4 10605 axacndlem5 10606 axacnd 10607 axextdist 34771 axextbdist 34772 distel 34775 wl-cbvalnaed 36401 wl-2sb6d 36423 wl-sbalnae 36427 wl-mo2df 36435 wl-mo2tf 36436 wl-eudf 36437 wl-eutf 36438 ax6e2ndeq 43320 ax6e2ndeqVD 43670 |
Copyright terms: Public domain | W3C validator |