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 2138 | . 2 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑) | |
2 | 1 | nf5i 2141 | 1 ⊢ Ⅎ𝑥∃𝑥𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ∃wex 1771 Ⅎwnf 1775 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-10 2136 |
This theorem depends on definitions: df-bi 208 df-ex 1772 df-nf 1776 |
This theorem is referenced by: nfa1 2146 nfnf1 2149 nf6 2282 exdistrf 2461 nfeu1ALT 2668 euor2 2690 2moexv 2705 moexexvw 2706 2moswapv 2707 2euexv 2709 eupicka 2712 mopick2 2715 moexex 2716 2moex 2718 2euex 2719 2moswap 2722 2mo 2726 2eu7 2738 2eu8 2739 nfre1 3303 ceqsexg 3643 morex 3707 intab 4897 nfopab1 5126 nfopab2 5127 axrep1 5182 axrep2 5184 axrep3 5185 axrep4 5186 eusv2nf 5286 copsexgw 5372 copsexg 5373 copsex2t 5374 copsex2g 5375 mosubopt 5391 dfid3 5455 dmcoss 5835 imadif 6431 oprabidw 7176 nfoprab1 7204 nfoprab2 7205 nfoprab3 7206 fsplitOLD 7802 zfcndrep 10024 zfcndpow 10026 zfcndreg 10027 zfcndinf 10028 reclem2pr 10458 ex-natded9.26 28125 brabgaf 30287 bnj607 32087 bnj849 32096 bnj1398 32203 bnj1449 32217 finminlem 33563 exisym1 33669 bj-alexbiex 33930 bj-exexbiex 33931 bj-biexal2 33937 bj-biexex 33940 bj-sbf3 34059 copsex2d 34323 sbexi 35272 ac6s6 35331 e2ebind 40774 e2ebindVD 41123 e2ebindALT 41140 stoweidlem57 42219 ovncvrrp 42723 ich2ex 43506 ichreuopeq 43512 reuopreuprim 43565 |
Copyright terms: Public domain | W3C validator |