![]() |
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 2375. Use the weaker nfnaew 2147 when possible. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) |
Ref | Expression |
---|---|
nfnae | ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfae 2436 | . 2 ⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦 | |
2 | 1 | nfn 1855 | 1 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∀wal 1535 Ⅎwnf 1780 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-10 2139 ax-11 2155 ax-12 2175 ax-13 2375 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1540 df-ex 1777 df-nf 1781 |
This theorem is referenced by: nfald2 2448 dvelimf 2451 sbequ6 2469 2ax6elem 2473 nfsb4t 2502 sbco2 2514 sbco3 2516 sb9 2522 sbal1 2531 sbal2 2532 nfabd2 2927 ralcom2 3375 dfid3 5586 nfriotad 7399 axextnd 10629 axrepndlem1 10630 axrepndlem2 10631 axrepnd 10632 axunndlem1 10633 axunnd 10634 axpowndlem2 10636 axpowndlem3 10637 axpowndlem4 10638 axpownd 10639 axregndlem2 10641 axregnd 10642 axinfndlem1 10643 axinfnd 10644 axacndlem4 10648 axacndlem5 10649 axacnd 10650 axnulg 35085 axextdist 35781 axextbdist 35782 distel 35785 wl-cbvalnaed 37513 wl-2sb6d 37539 wl-sbalnae 37543 wl-mo2df 37551 wl-mo2tf 37552 wl-eudf 37553 wl-eutf 37554 ax6e2ndeq 44557 ax6e2ndeqVD 44907 |
Copyright terms: Public domain | W3C validator |