![]() |
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 2061 | . 2 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑) | |
2 | 1 | nf5i 2064 | 1 ⊢ Ⅎ𝑥∃𝑥𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ∃wex 1744 Ⅎwnf 1748 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-10 2059 |
This theorem depends on definitions: df-bi 197 df-ex 1745 df-nf 1750 |
This theorem is referenced by: nfa1 2068 nfnf1 2071 nf6 2155 exdistrf 2364 nfmo1 2509 euor2 2543 eupicka 2566 mopick2 2569 moexex 2570 2moex 2572 2euex 2573 2moswap 2576 2mo 2580 2eu7 2588 2eu8 2589 nfre1 3034 ceqsexg 3365 morex 3423 intab 4539 nfopab1 4752 nfopab2 4753 axrep1 4805 axrep2 4806 axrep3 4807 axrep4 4808 eusv2nf 4894 copsexg 4985 copsex2t 4986 copsex2g 4987 mosubopt 5001 dfid3 5054 dmcoss 5417 imadif 6011 nfoprab1 6746 nfoprab2 6747 nfoprab3 6748 fsplit 7327 zfcndrep 9474 zfcndpow 9476 zfcndreg 9477 zfcndinf 9478 reclem2pr 9908 ex-natded9.26 27406 brabgaf 29546 bnj607 31112 bnj849 31121 bnj1398 31228 bnj1449 31242 finminlem 32437 exisym1 32548 bj-alexbiex 32815 bj-exexbiex 32816 bj-biexal2 32822 bj-biexex 32825 bj-axrep1 32913 bj-axrep2 32914 bj-axrep3 32915 bj-axrep4 32916 bj-sbf3 32951 sbexi 34046 ac6s6 34110 e2ebind 39096 e2ebindVD 39462 e2ebindALT 39479 stoweidlem57 40592 ovncvrrp 41099 |
Copyright terms: Public domain | W3C validator |