![]() |
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 3061 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
2 | nfe1 2140 | . 2 ⊢ Ⅎ𝑥∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) | |
3 | 1, 2 | nfxfr 1848 | 1 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 394 ∃wex 1774 Ⅎwnf 1778 ∈ wcel 2099 ∃wrex 3060 |
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 df-rex 3061 |
This theorem is referenced by: 2rmorex 3748 2reurex 3754 reuan 3889 2reu4lem 4530 nfiu1 5035 nfiu1OLD 5036 reusv2lem3 5404 fvelimad 6970 fsnex 7297 eusvobj2 7416 fiun 7956 f1iun 7957 zfregcl 9637 scott0 9929 ac6c4 10524 lbzbi 12972 mreiincl 17609 lss1d 20940 neiptopnei 23127 neitr 23175 utopsnneiplem 24243 cfilucfil 24559 2sqmo 27466 nosupbnd2 27746 noinfbnd2 27761 mptelee 28829 isch3 31174 atom1d 32286 opreu2reuALT 32405 iinabrex 32489 xrofsup 32671 locfinreflem 33655 esumc 33884 esumrnmpt2 33901 hasheuni 33918 esumcvg 33919 esumcvgre 33924 voliune 34062 volfiniune 34063 ddemeas 34069 eulerpartlemgvv 34210 bnj900 34774 bnj1189 34854 bnj1204 34857 bnj1398 34879 bnj1444 34888 bnj1445 34889 bnj1446 34890 bnj1447 34891 bnj1467 34899 bnj1518 34909 bnj1519 34910 iooelexlt 37069 fvineqsneq 37119 ptrest 37320 poimirlem26 37347 indexa 37434 filbcmb 37441 sdclem1 37444 heibor1 37511 dihglblem5 40997 unielss 42883 oaun3lem1 43040 suprnmpt 44781 disjinfi 44799 upbdrech 44920 ssfiunibd 44924 infxrunb2 44983 supxrunb3 45014 iccshift 45136 iooshift 45140 islpcn 45260 limsupre 45262 limclner 45272 limsupre3uzlem 45356 climuzlem 45364 xlimmnfv 45455 xlimpnfv 45459 itgperiod 45602 stoweidlem53 45674 stoweidlem57 45678 fourierdlem48 45775 fourierdlem51 45778 fourierdlem73 45800 fourierdlem81 45808 elaa2 45855 etransclem32 45887 sge0iunmptlemre 46036 voliunsge0lem 46093 meaiuninc3v 46105 isomenndlem 46151 ovnsubaddlem1 46191 hoidmvlelem1 46216 hoidmvlelem5 46220 smfaddlem1 46384 tworepnotupword 46505 2reu7 46724 2reu8 46725 f1oresf1o2 46904 mogoldbb 47357 2zrngagrp 47626 2zrngmmgm 47629 |
Copyright terms: Public domain | W3C validator |