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 2153 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 1864 | 1 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∀wal 1540 Ⅎwnf 1790 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-10 2145 ax-11 2162 ax-12 2179 ax-13 2372 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-tru 1545 df-ex 1787 df-nf 1791 |
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 2925 ralcom2 3266 dfid3 5431 nfriotad 7139 axextnd 10091 axrepndlem1 10092 axrepndlem2 10093 axrepnd 10094 axunndlem1 10095 axunnd 10096 axpowndlem2 10098 axpowndlem3 10099 axpowndlem4 10100 axpownd 10101 axregndlem2 10103 axregnd 10104 axinfndlem1 10105 axinfnd 10106 axacndlem4 10110 axacndlem5 10111 axacnd 10112 axextdist 33347 axextbdist 33348 distel 33351 wl-cbvalnaed 35314 wl-2sb6d 35336 wl-sbalnae 35340 wl-mo2df 35348 wl-mo2tf 35349 wl-eudf 35350 wl-eutf 35351 ax6e2ndeq 41717 ax6e2ndeqVD 42067 |
Copyright terms: Public domain | W3C validator |