| 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 1785 changed. (Revised by Wolf Lammen, 11-Sep-2021.) Remove dependency on ax-12 2184. (Revised by Wolf Lammen, 12-Oct-2021.) |
| Ref | Expression |
|---|---|
| nfa1 | ⊢ Ⅎ𝑥∀𝑥𝜑 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | alex 1827 | . 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑) | |
| 2 | nfe1 2155 | . . 3 ⊢ Ⅎ𝑥∃𝑥 ¬ 𝜑 | |
| 3 | 2 | nfn 1858 | . 2 ⊢ Ⅎ𝑥 ¬ ∃𝑥 ¬ 𝜑 |
| 4 | 1, 3 | nfxfr 1854 | 1 ⊢ Ⅎ𝑥∀𝑥𝜑 |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 ∀wal 1539 ∃wex 1780 Ⅎwnf 1784 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-10 2146 |
| This theorem depends on definitions: df-bi 207 df-or 848 df-ex 1781 df-nf 1785 |
| This theorem is referenced by: nfna1 2157 nfia1 2158 nfnf1 2159 nfs1v 2161 nfa2 2181 sbalexOLD 2250 sbf2 2278 equs5av 2283 nf5 2288 hba1 2299 axc4i 2327 19.12 2332 exsb 2363 equs5aALT 2370 equs5eALT 2371 cbv1h 2409 dral1 2443 nfald2 2449 equs5a 2461 equs5e 2462 equs5 2464 axc14 2467 nfsb4t 2503 sbcom3 2510 moexexlem 2626 2eu6 2657 axi12 2706 nfaba1 2906 nfaba1OLD 2907 nfaba1g 2908 nfra1 3260 ceqsalgALT 3477 elrab3t 3645 csbie2t 3887 rexdifi 4102 sbcnestgfw 4373 sbcnestgf 4378 dfnfc2 4885 mpteq12f 5183 axrep2 5227 axrep3 5228 axrep4OLD 5231 alxfr 5352 axprlem4OLD 5374 axprlem5OLD 5375 copsex2t 5440 mosubopt 5458 fv3 6852 fvmptt 6961 fnoprabg 7481 pssnn 9093 fiint 9227 aceq1 10027 zorn2lem4 10409 zfcndrep 10525 mreexexd 17571 dvelimalcased 35231 dvelimexcased 35233 fineqvrep 35270 dfon2lem7 35981 mh-setindnd 36667 bj-alalbial 36902 bj-exalbial 36903 bj-biexal1 36906 bj-bialal 36909 bj-cbv1hv 36997 ax11-pm 37033 bj-snsetex 37164 exlimim 37543 exellim 37545 difunieq 37575 fvineqsneq 37613 wl-nfimf1 37727 wl-nfae1 37728 wl-sb8t 37753 wl-sbnf1 37756 wl-2spsbbi 37766 wl-lem-moexsb 37769 wl-mo2tf 37772 wl-eutf 37774 wl-mo2t 37776 wl-mo3t 37777 wl-sb8eut 37779 sbali 38309 setindtr 43262 unielss 43456 ismnushort 44538 axc11next 44643 pm14.122b 44660 pm14.123b 44663 ax6e2ndeqVD 45145 e2ebindALT 45165 ax6e2ndeqALT 45167 modelaxreplem2 45216 modelaxreplem3 45217 permaxrep 45243 rexsb 47341 nfich1 47689 ichnfimlem 47705 ich2al 47709 pgind 49958 |
| Copyright terms: Public domain | W3C validator |