![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfre1 | Structured version Visualization version GIF version |
Description: The setvar 𝑥 is not free in ∃𝑥 ∈ 𝐴𝜑. (Contributed by NM, 19-Mar-1997.) (Revised by Mario Carneiro, 7-Oct-2016.) |
Ref | Expression |
---|---|
nfre1 | ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rex 3071 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
2 | nfe1 2148 | . 2 ⊢ Ⅎ𝑥∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) | |
3 | 1, 2 | nfxfr 1856 | 1 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 397 ∃wex 1782 Ⅎwnf 1786 ∈ wcel 2107 ∃wrex 3070 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-10 2138 |
This theorem depends on definitions: df-bi 206 df-ex 1783 df-nf 1787 df-rex 3071 |
This theorem is referenced by: 2rmorex 3713 2reurex 3719 reuan 3853 2reu4lem 4484 nfiu1 4989 reusv2lem3 5356 fvelimad 6910 fsnex 7230 eusvobj2 7350 fiun 7876 f1iun 7877 zfregcl 9535 scott0 9827 ac6c4 10422 lbzbi 12866 mreiincl 17481 lss1d 20439 neiptopnei 22499 neitr 22547 utopsnneiplem 23615 cfilucfil 23931 2sqmo 26801 nosupbnd2 27080 noinfbnd2 27095 mptelee 27886 isch3 30225 atom1d 31337 opreu2reuALT 31448 iinabrex 31533 xrofsup 31719 locfinreflem 32478 esumc 32707 esumrnmpt2 32724 hasheuni 32741 esumcvg 32742 esumcvgre 32747 voliune 32885 volfiniune 32886 ddemeas 32892 eulerpartlemgvv 33033 bnj900 33598 bnj1189 33678 bnj1204 33681 bnj1398 33703 bnj1444 33712 bnj1445 33713 bnj1446 33714 bnj1447 33715 bnj1467 33723 bnj1518 33733 bnj1519 33734 iooelexlt 35879 fvineqsneq 35929 ptrest 36123 poimirlem26 36150 indexa 36238 filbcmb 36245 sdclem1 36248 heibor1 36315 dihglblem5 39807 unielss 41595 oaun3lem1 41733 suprnmpt 43479 disjinfi 43500 upbdrech 43626 ssfiunibd 43630 infxrunb2 43689 supxrunb3 43720 iccshift 43842 iooshift 43846 islpcn 43966 limsupre 43968 limclner 43978 limsupre3uzlem 44062 climuzlem 44070 xlimmnfv 44161 xlimpnfv 44165 itgperiod 44308 stoweidlem53 44380 stoweidlem57 44384 fourierdlem48 44481 fourierdlem51 44484 fourierdlem73 44506 fourierdlem81 44514 elaa2 44561 etransclem32 44593 sge0iunmptlemre 44742 voliunsge0lem 44799 meaiuninc3v 44811 isomenndlem 44857 ovnsubaddlem1 44897 hoidmvlelem1 44922 hoidmvlelem5 44926 smfaddlem1 45090 tworepnotupword 45211 2reu7 45429 2reu8 45430 f1oresf1o2 45609 mogoldbb 46063 2zrngagrp 46327 2zrngmmgm 46330 |
Copyright terms: Public domain | W3C validator |