| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > nfa1 | Structured version Visualization version GIF version | ||
| Description: The setvar 𝑥 is not free in ∀𝑥𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1784 changed. (Revised by Wolf Lammen, 11-Sep-2021.) Remove dependency on ax-12 2177. (Revised by Wolf Lammen, 12-Oct-2021.) |
| Ref | Expression |
|---|---|
| nfa1 | ⊢ Ⅎ𝑥∀𝑥𝜑 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | alex 1826 | . 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑) | |
| 2 | nfe1 2150 | . . 3 ⊢ Ⅎ𝑥∃𝑥 ¬ 𝜑 | |
| 3 | 2 | nfn 1857 | . 2 ⊢ Ⅎ𝑥 ¬ ∃𝑥 ¬ 𝜑 |
| 4 | 1, 3 | nfxfr 1853 | 1 ⊢ Ⅎ𝑥∀𝑥𝜑 |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 ∀wal 1538 ∃wex 1779 Ⅎ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-10 2141 |
| This theorem depends on definitions: df-bi 207 df-or 849 df-ex 1780 df-nf 1784 |
| This theorem is referenced by: nfna1 2152 nfia1 2153 nfnf1 2154 nfs1v 2156 nfa2 2176 sbalexOLD 2243 sbf2 2272 equs5av 2277 nf5 2282 hba1 2293 axc4i 2322 19.12 2327 exsb 2362 equs5aALT 2369 equs5eALT 2370 dral1vOLD 2373 cbv1h 2410 dral1 2444 nfald2 2450 equs5a 2462 equs5e 2463 equs5 2465 axc14 2468 nfsb4t 2504 sbcom3 2511 nfmo1 2557 nfeu1 2588 moexexlem 2626 2eu6 2657 axi12 2706 nfaba1 2913 nfaba1OLD 2914 nfaba1g 2915 nfra1 3284 nfra2wOLD 3300 ceqsalgALT 3518 elrab3t 3691 csbie2t 3937 rexdifi 4150 sbcnestgfw 4421 sbcnestgf 4426 dfnfc2 4929 mpteq12f 5230 axrep2 5282 axrep3 5283 axrep4OLD 5286 alxfr 5407 axprlem4OLD 5429 axprlem5OLD 5430 copsex2t 5497 mosubopt 5515 fv3 6924 fvmptt 7036 fnoprabg 7556 pssnn 9208 fiint 9366 fiintOLD 9367 aceq1 10157 zorn2lem4 10539 zfcndrep 10654 mreexexd 17691 dvelimalcased 35089 dvelimexcased 35091 fineqvrep 35109 dfon2lem7 35790 bj-alalbial 36702 bj-exalbial 36703 bj-biexal1 36706 bj-bialal 36709 bj-cbv1hv 36797 ax11-pm 36833 bj-snsetex 36964 exlimim 37343 exellim 37345 difunieq 37375 fvineqsneq 37413 wl-nfimf1 37527 wl-nfae1 37528 wl-sb8t 37553 wl-sbnf1 37556 wl-2spsbbi 37566 wl-lem-moexsb 37569 wl-mo2tf 37572 wl-eutf 37574 wl-mo2t 37576 wl-mo3t 37577 wl-sb8eut 37579 wl-ax11-lem3 37588 sbali 38119 setindtr 43036 unielss 43230 ismnushort 44320 axc11next 44425 pm14.122b 44442 pm14.123b 44445 eubiOLD 44455 ax6e2ndeqVD 44929 e2ebindALT 44949 ax6e2ndeqALT 44951 modelaxreplem2 44996 modelaxreplem3 44997 rexsb 47111 nfich1 47434 ichnfimlem 47450 ich2al 47454 pgind 49236 |
| Copyright terms: Public domain | W3C validator |