![]() |
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 2132 | . 2 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑) | |
2 | 1 | nf5i 2135 | 1 ⊢ Ⅎ𝑥∃𝑥𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ∃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-ex 1775 df-nf 1779 |
This theorem is referenced by: nfa1 2141 nfnf1 2144 nf6 2273 exdistrf 2442 nfeu1ALT 2579 euor2 2605 2moexv 2619 moexexvw 2620 2moswapv 2621 2euexv 2623 eupicka 2626 mopick2 2629 moexex 2630 2moex 2632 2euex 2633 2moswap 2636 2mo 2640 2eu7 2649 2eu8 2650 nfre1 3278 ceqsexg 3638 morex 3713 intab 4977 nfopab1 5213 nfopab2 5214 axrep1 5281 axrep2 5283 axrep3 5284 axrep4 5285 eusv2nf 5390 copsexgw 5487 copsexg 5488 copsex2t 5489 copsex2gOLD 5491 mosubopt 5507 dfid3 5574 dmcoss 5969 imadif 6632 oprabidw 7446 nfoprab1 7476 nfoprab2 7477 nfoprab3 7478 zfcndrep 10632 zfcndpow 10634 zfcndreg 10635 zfcndinf 10636 reclem2pr 11066 ex-natded9.26 30223 brabgaf 32392 bnj607 34542 bnj849 34551 bnj1398 34660 bnj1449 34674 finminlem 35797 exisym1 35903 bj-alexbiex 36171 bj-exexbiex 36172 bj-biexal2 36178 bj-biexex 36181 bj-sbf3 36311 copsex2d 36613 sbexi 37581 ac6s6 37640 e2ebind 43993 e2ebindVD 44342 e2ebindALT 44359 stoweidlem57 45436 ovncvrrp 45943 ich2ex 46799 ichreuopeq 46804 reuopreuprim 46857 pgind 48139 |
Copyright terms: Public domain | W3C validator |