![]() |
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 1747 changed. (Revised by Wolf Lammen, 11-Sep-2021.) Remove dependency on ax-12 2104. (Revised by Wolf Lammen, 12-Oct-2021.) |
Ref | Expression |
---|---|
nfa1 | ⊢ Ⅎ𝑥∀𝑥𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alex 1788 | . 2 ⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑) | |
2 | nfe1 2085 | . . 3 ⊢ Ⅎ𝑥∃𝑥 ¬ 𝜑 | |
3 | 2 | nfn 1819 | . 2 ⊢ Ⅎ𝑥 ¬ ∃𝑥 ¬ 𝜑 |
4 | 1, 3 | nfxfr 1815 | 1 ⊢ Ⅎ𝑥∀𝑥𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∀wal 1505 ∃wex 1742 Ⅎwnf 1746 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-10 2077 |
This theorem depends on definitions: df-bi 199 df-or 834 df-ex 1743 df-nf 1747 |
This theorem is referenced by: nfna1 2087 nfia1 2088 nfnf1 2089 nfa2 2103 sbf2 2198 nfs1v 2200 sb56OLD 2205 nf5 2214 hba1 2225 spsbimvOLD 2249 axc4i 2260 19.12 2265 exsb 2290 equs5aALT 2296 equs5eALT 2297 cbv1h 2336 axc15OLD 2356 dral1 2373 nfald2 2379 equs5a 2392 equs5e 2393 equs5 2395 axc14 2398 exsbOLD 2420 nfsb4t 2458 sbcom3 2470 nfsb4tALT 2528 nfmo1 2566 nfeu1 2602 moexexvw 2656 2moswapv 2657 moexex 2664 2eu6 2683 exists2OLD 2690 axi12 2741 nfaba1 2933 nfra1 3163 ceqsalgALT 3445 elrab3t 3588 sbcbi2 3730 csbie2t 3813 sbcnestgf 4253 dfnfc2 4724 mpteq12f 5004 axrep2 5046 axrep3 5047 axrep4 5048 alxfr 5155 axprlem4 5177 axprlem5 5178 copsex2t 5232 mosubopt 5249 fv3 6511 fvmptt 6608 fnoprabg 7085 pssnn 8523 fiint 8582 aceq1 9329 zorn2lem4 9711 zfcndrep 9826 mreexexd 16767 dfon2lem7 32494 bj-alalbial 33484 bj-exalbial 33485 bj-biexal1 33488 bj-bialal 33491 bj-cbv1hv 33517 bj-dral1v 33533 bj-axrep2 33559 bj-axrep3 33560 bj-axrep4 33561 ax11-pm 33586 bj-snsetex 33728 exlimim 34000 exellim 34002 difunieq 34032 fvineqsneq 34069 wl-nfimf1 34145 wl-nfae1 34146 wl-sb8t 34165 wl-sbnf1 34168 wl-2spsbbi 34178 wl-ich-lem1 34180 wl-ich-lem1b 34182 wl-ich-lem1d 34185 wl-lem-moexsb 34193 wl-mo2tf 34196 wl-eutf 34198 wl-mo2t 34200 wl-mo3t 34201 wl-sb8eut 34202 wl-ax11-lem3 34208 sbali 34782 setindtr 38962 axc11next 40099 pm14.122b 40116 pm14.123b 40119 eubiOLD 40129 ax6e2ndeqVD 40606 e2ebindALT 40626 ax6e2ndeqALT 40628 rexsb 42649 nfich1 42925 dfich2bi 42930 |
Copyright terms: Public domain | W3C validator |