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. See also nfnaew 2144. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Ref | Expression |
---|---|
nfnae | ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfae 2447 | . 2 ⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦 | |
2 | 1 | nfn 1848 | 1 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∀wal 1526 Ⅎwnf 1775 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-10 2136 ax-11 2151 ax-12 2167 ax-13 2381 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 |
This theorem is referenced by: nfald2 2459 dvelimf 2462 sbequ6 2481 2ax6elem 2485 nfsb4t 2532 sbco2 2546 sbco3 2548 sb9 2554 sbal1 2565 sbal2 2566 sbal2OLD 2567 nfsb4tALT 2597 sbco2ALT 2608 axbndOLD 2789 nfabd2 2999 nfabd2OLD 3000 ralcom2 3361 dfid3 5455 nfriotad 7114 axextnd 10001 axrepndlem1 10002 axrepndlem2 10003 axrepnd 10004 axunndlem1 10005 axunnd 10006 axpowndlem2 10008 axpowndlem3 10009 axpowndlem4 10010 axpownd 10011 axregndlem2 10013 axregnd 10014 axinfndlem1 10015 axinfnd 10016 axacndlem4 10020 axacndlem5 10021 axacnd 10022 axextdist 32941 axextbdist 32942 distel 32945 wl-cbvalnaed 34653 wl-2sb6d 34675 wl-sbalnae 34679 wl-mo2df 34687 wl-mo2tf 34688 wl-eudf 34689 wl-eutf 34690 ax6e2ndeq 40770 ax6e2ndeqVD 41120 |
Copyright terms: Public domain | W3C validator |