![]() |
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 1779 changed. (Revised by Wolf Lammen, 11-Sep-2021.) Remove dependency on ax-12 2167. (Revised by Wolf Lammen, 12-Oct-2021.) |
Ref | Expression |
---|---|
nfa1 | ⊢ Ⅎ𝑥∀𝑥𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alex 1821 | . 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑) | |
2 | nfe1 2140 | . . 3 ⊢ Ⅎ𝑥∃𝑥 ¬ 𝜑 | |
3 | 2 | nfn 1853 | . 2 ⊢ Ⅎ𝑥 ¬ ∃𝑥 ¬ 𝜑 |
4 | 1, 3 | nfxfr 1848 | 1 ⊢ Ⅎ𝑥∀𝑥𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∀wal 1532 ∃wex 1774 Ⅎwnf 1778 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-10 2130 |
This theorem depends on definitions: df-bi 206 df-or 846 df-ex 1775 df-nf 1779 |
This theorem is referenced by: nfna1 2142 nfia1 2143 nfnf1 2144 nfs1v 2146 nfa2 2166 sbalex 2231 sbf2 2259 equs5av 2266 nf5 2272 hba1 2283 axc4i 2311 19.12 2316 exsb 2350 equs5aALT 2358 equs5eALT 2359 dral1vOLD 2362 cbv1h 2399 dral1 2433 nfald2 2439 equs5a 2451 equs5e 2452 equs5 2454 axc14 2457 nfsb4t 2493 sbcom3 2500 nfmo1 2546 nfeu1 2577 moexexlem 2615 2eu6 2646 axi12 2695 nfaba1 2900 nfaba1OLD 2901 nfaba1g 2902 nfabdwOLD 2917 nfra1 3272 nfra2wOLD 3288 ceqsalgALT 3499 elrab3t 3680 csbie2t 3933 rexdifi 4145 sbcnestgfw 4423 sbcnestgf 4428 dfnfc2 4937 mpteq12f 5241 axrep2 5293 axrep3 5294 axrep4 5295 alxfr 5411 axprlem4 5430 axprlem5 5431 copsex2t 5498 mosubopt 5516 fv3 6919 fvmptt 7029 fnoprabg 7548 pssnn 9206 pssnnOLD 9299 fiint 9368 fiintOLD 9369 aceq1 10160 zorn2lem4 10542 zfcndrep 10657 mreexexd 17661 fineqvrep 34931 dfon2lem7 35613 bj-alalbial 36406 bj-exalbial 36407 bj-biexal1 36410 bj-bialal 36413 bj-cbv1hv 36501 ax11-pm 36537 bj-snsetex 36670 exlimim 37049 exellim 37051 difunieq 37081 fvineqsneq 37119 wl-nfimf1 37221 wl-nfae1 37222 wl-sb8t 37247 wl-sbnf1 37250 wl-2spsbbi 37260 wl-lem-moexsb 37263 wl-mo2tf 37266 wl-eutf 37268 wl-mo2t 37270 wl-mo3t 37271 wl-sb8eut 37273 wl-ax11-lem3 37282 sbali 37813 setindtr 42682 unielss 42883 ismnushort 43975 axc11next 44080 pm14.122b 44097 pm14.123b 44100 eubiOLD 44110 ax6e2ndeqVD 44585 e2ebindALT 44605 ax6e2ndeqALT 44607 rexsb 46712 nfich1 47019 ichnfimlem 47035 ich2al 47039 pgind 48463 |
Copyright terms: Public domain | W3C validator |