| 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 1807 changed. (Revised by Wolf Lammen, 11-Sep-2021.) Remove dependency on ax-12 2215. (Revised by Wolf Lammen, 12-Oct-2021.) |
| Ref | Expression |
|---|---|
| nfa1 | ⊢ Ⅎ𝑥∀𝑥𝜑 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | alex 1849 | . 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑) | |
| 2 | nfe1 2187 | . . 3 ⊢ Ⅎ𝑥∃𝑥 ¬ 𝜑 | |
| 3 | 2 | nfn 1880 | . 2 ⊢ Ⅎ𝑥 ¬ ∃𝑥 ¬ 𝜑 |
| 4 | 1, 3 | nfxfr 1876 | 1 ⊢ Ⅎ𝑥∀𝑥𝜑 |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 ∀wal 1561 ∃wex 1802 Ⅎwnf 1806 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-10 2178 |
| This theorem depends on definitions: df-bi 210 df-or 861 df-ex 1803 df-nf 1807 |
| This theorem is referenced by: nfna1 2189 nfia1 2190 nfnf1 2191 nfs1v 2193 nfa2 2212 sbalexOLD 2281 sbf2 2309 equs5av 2314 nf5 2319 hba1 2330 axc4i 2357 19.12 2362 exsb 2393 equs5aALT 2400 equs5eALT 2401 cbv1h 2439 dral1 2473 nfald2 2479 equs5a 2491 equs5e 2492 equs5 2494 axc14 2497 nfsb4t 2533 sbcom3 2540 moexexlem 2656 2eu6 2686 axi12 2735 nfaba1 2935 nfaba1g 2936 nfra1 3289 ceqsalgALT 3493 elrab3t 3652 csbie2t 3893 rexdifi 4106 sbcnestgfw 4378 sbcnestgf 4383 dfnfc2 4890 mpteq12f 5190 axrep2 5235 axrep3 5236 axrep4OLD 5239 alxfr 5369 axprlem4OLD 5392 axprlem5OLD 5393 copsex2t 5466 mosubopt 5484 fv3 6889 fvmptt 7000 fnoprabg 7523 pssnn 9141 fiint 9274 aceq1 10089 zorn2lem4 10471 zfcndrep 10587 mreexexd 17694 dvelimalcased 35380 dvelimexcased 35382 fineqvrep 35422 axsepg4 35451 dfon2lem7 36150 mh-setindnd 36910 bj-alalbial 37188 bj-exalbial 37189 bj-biexal1 37192 bj-bialal 37195 bj-cbv1hv 37293 ax11-pm 37329 bj-snsetex 37460 exlimim 37848 exellim 37850 difunieq 37880 fvineqsneq 37918 wl-nfimf1 38041 wl-nfae1 38042 wl-sb8t 38067 wl-sbnf1 38070 wl-2spsbbi 38080 wl-lem-moexsb 38083 wl-mo2tf 38086 wl-eutf 38088 wl-mo2t 38090 wl-mo3t 38091 wl-sb8eut 38093 sbali 38623 setindtr 43613 unielss 43807 ismnushort 44875 axc11next 44980 pm14.122b 44997 pm14.123b 45000 ax6e2ndeqVD 45482 e2ebindALT 45502 ax6e2ndeqALT 45504 modelaxreplem2 45553 modelaxreplem3 45554 permaxrep 45580 rexsb 47691 nfich1 48051 ichnfimlem 48067 ich2al 48071 pgind 50346 |
| Copyright terms: Public domain | W3C validator |