|   | 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 2377. Use the weaker nfnaew 2149 when possible. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) | 
| Ref | Expression | 
|---|---|
| nfnae | ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦 | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | nfae 2438 | . 2 ⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦 | |
| 2 | 1 | nfn 1857 | 1 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦 | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 ∀wal 1538 Ⅎwnf 1783 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-10 2141 ax-11 2157 ax-12 2177 ax-13 2377 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-nf 1784 | 
| This theorem is referenced by: nfald2 2450 dvelimf 2453 sbequ6 2471 2ax6elem 2475 nfsb4t 2504 sbco2 2516 sbco3 2518 sb9 2524 sbal1 2533 sbal2 2534 nfabd2 2929 ralcom2 3377 dfid3 5581 nfriotad 7399 axextnd 10631 axrepndlem1 10632 axrepndlem2 10633 axrepnd 10634 axunndlem1 10635 axunnd 10636 axpowndlem2 10638 axpowndlem3 10639 axpowndlem4 10640 axpownd 10641 axregndlem2 10643 axregnd 10644 axinfndlem1 10645 axinfnd 10646 axacndlem4 10650 axacndlem5 10651 axacnd 10652 axnulg 35106 axextdist 35800 axextbdist 35801 distel 35804 wl-cbvalnaed 37533 wl-2sb6d 37559 wl-sbalnae 37563 wl-mo2df 37571 wl-mo2tf 37572 wl-eudf 37573 wl-eutf 37574 ax6e2ndeq 44579 ax6e2ndeqVD 44929 | 
| Copyright terms: Public domain | W3C validator |