![]() |
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. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Ref | Expression |
---|---|
nfnae | ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfae 2446 | . 2 ⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦 | |
2 | 1 | nfn 1921 | 1 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∀wal 1618 Ⅎwnf 1845 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1859 ax-4 1874 ax-5 1976 ax-6 2042 ax-7 2078 ax-10 2156 ax-11 2171 ax-12 2184 ax-13 2379 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1623 df-ex 1842 df-nf 1847 |
This theorem is referenced by: nfald2 2459 dvelimf 2462 sbequ6 2513 nfsb4t 2514 sbco2 2540 sbco3 2542 sb9 2551 2ax6elem 2574 sbal1 2585 sbal2 2586 axbnd 2727 nfabd2 2910 ralcom2 3230 dfid3 5163 nfriotad 6770 axextnd 9576 axrepndlem1 9577 axrepndlem2 9578 axrepnd 9579 axunndlem1 9580 axunnd 9581 axpowndlem2 9583 axpowndlem3 9584 axpowndlem4 9585 axpownd 9586 axregndlem2 9588 axregnd 9589 axinfndlem1 9590 axinfnd 9591 axacndlem4 9595 axacndlem5 9596 axacnd 9597 axextdist 31981 axext4dist 31982 distel 31985 bj-axc14nf 33115 wl-cbvalnaed 33601 wl-2sb6d 33623 wl-sbalnae 33627 wl-mo2df 33634 wl-mo2tf 33635 wl-eudf 33636 wl-eutf 33637 wl-euequ1f 33638 ax6e2ndeq 39246 ax6e2ndeqVD 39613 |
Copyright terms: Public domain | W3C validator |