| 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 2143 | . 2 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑) | |
| 2 | 1 | nf5i 2146 | 1 ⊢ Ⅎ𝑥∃𝑥𝜑 |
| Colors of variables: wff setvar class |
| Syntax hints: ∃wex 1779 Ⅎwnf 1783 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-10 2141 |
| This theorem depends on definitions: df-bi 207 df-ex 1780 df-nf 1784 |
| This theorem is referenced by: nfa1 2151 nfnf1 2154 sbalex 2242 nf6 2283 exdistrf 2452 nfeu1ALT 2589 euor2 2613 2moexv 2627 moexexvw 2628 2moswapv 2629 2euexv 2631 eupicka 2634 mopick2 2637 moexex 2638 2moex 2640 2euex 2641 2moswap 2644 2mo 2648 2eu7 2658 2eu8 2659 nfre1 3285 ceqsexg 3653 morex 3725 intab 4978 nfopab1 5213 nfopab2 5214 axrep1 5280 axrep2 5282 axrep3 5283 axrep4OLD 5286 eusv2nf 5395 copsexgw 5495 copsexg 5496 copsex2t 5497 mosubopt 5515 dfid3 5581 dmcoss 5985 imadif 6650 oprabidw 7462 nfoprab1 7494 nfoprab2 7495 nfoprab3 7496 zfcndrep 10654 zfcndpow 10656 zfcndreg 10657 zfcndinf 10658 reclem2pr 11088 ex-natded9.26 30438 brabgaf 32620 bnj607 34930 bnj849 34939 bnj1398 35048 bnj1449 35062 finminlem 36319 exisym1 36425 bj-alexbiex 36700 bj-exexbiex 36701 bj-biexal2 36707 bj-biexex 36710 bj-sbf3 36840 copsex2d 37140 sbexi 38120 ac6s6 38179 e2ebind 44583 e2ebindVD 44932 e2ebindALT 44949 stoweidlem57 46072 ovncvrrp 46579 ich2ex 47455 ichreuopeq 47460 reuopreuprim 47513 pgind 49236 |
| Copyright terms: Public domain | W3C validator |