![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfe1 | Structured version Visualization version GIF version |
Description: The setvar 𝑥 is not free in ∃𝑥𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Ref | Expression |
---|---|
nfe1 | ⊢ Ⅎ𝑥∃𝑥𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hbe1 2137 | . 2 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑) | |
2 | 1 | nf5i 2140 | 1 ⊢ Ⅎ𝑥∃𝑥𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ∃wex 1823 Ⅎwnf 1827 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-10 2135 |
This theorem depends on definitions: df-bi 199 df-ex 1824 df-nf 1828 |
This theorem is referenced by: nfa1 2145 nfnf1 2148 nf6 2257 exdistrf 2413 nfeu1ALT 2610 nfmo1OLD 2622 euor2 2648 eupicka 2664 mopick2 2667 moexex 2668 2moex 2670 2euex 2671 2moswap 2674 2mo 2678 2eu7 2688 2eu8 2689 nfre1 3186 ceqsexg 3537 morex 3602 intab 4742 nfopab1 4957 nfopab2 4958 axrep1 5009 axrep2 5011 axrep3 5012 axrep4 5013 eusv2nf 5109 copsexg 5189 copsex2t 5190 copsex2g 5191 mosubopt 5209 dfid3 5264 dmcoss 5633 imadif 6220 nfoprab1 6983 nfoprab2 6984 nfoprab3 6985 fsplit 7565 zfcndrep 9773 zfcndpow 9775 zfcndreg 9776 zfcndinf 9777 reclem2pr 10207 ex-natded9.26 27868 brabgaf 30000 bnj607 31593 bnj849 31602 bnj1398 31709 bnj1449 31723 finminlem 32909 exisym1 33014 bj-alexbiex 33286 bj-exexbiex 33287 bj-biexal2 33293 bj-biexex 33296 bj-axrep1 33373 bj-axrep2 33374 bj-axrep3 33375 bj-axrep4 33376 bj-sbf3 33409 sbexi 34548 ac6s6 34612 e2ebind 39737 e2ebindVD 40095 e2ebindALT 40112 stoweidlem57 41215 ovncvrrp 41719 |
Copyright terms: Public domain | W3C validator |