![]() |
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 3087 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
2 | nfe1 2088 | . 2 ⊢ Ⅎ𝑥∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) | |
3 | 1, 2 | nfxfr 1816 | 1 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 387 ∃wex 1743 Ⅎwnf 1747 ∈ wcel 2051 ∃wrex 3082 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-10 2080 |
This theorem depends on definitions: df-bi 199 df-ex 1744 df-nf 1748 df-rex 3087 |
This theorem is referenced by: r19.29anOLD 3266 2rmorex 3647 2reurex 3652 reuan 3776 2reu4lem 4342 nfiu1 4819 reusv2lem3 5150 fvelimad 6559 fsnex 6862 eusvobj2 6967 fun11iun 7456 zfregcl 8851 scott0 9107 ac6c4 9699 lbzbi 12148 mreiincl 16737 lss1d 19469 neiptopnei 21459 neitr 21507 utopsnneiplem 22574 cfilucfil 22887 2sqmo 25730 mptelee 26399 isch3 28812 atom1d 29926 opreu2reuALT 30037 xrofsup 30268 locfinreflem 30780 esumc 30986 esumrnmpt2 31003 hasheuni 31020 esumcvg 31021 esumcvgre 31026 voliune 31165 volfiniune 31166 ddemeas 31172 eulerpartlemgvv 31311 bnj900 31880 bnj1189 31958 bnj1204 31961 bnj1398 31983 bnj1444 31992 bnj1445 31993 bnj1446 31994 bnj1447 31995 bnj1467 32003 bnj1518 32013 bnj1519 32014 nosupbnd2 32774 iooelexlt 34122 fvineqsneq 34171 ptrest 34369 poimirlem26 34396 indexa 34487 filbcmb 34494 sdclem1 34497 heibor1 34567 dihglblem5 37916 suprnmpt 40888 disjinfi 40912 upbdrech 41033 ssfiunibd 41037 infxrunb2 41097 supxrunb3 41134 iccshift 41257 iooshift 41261 islpcn 41383 limsupre 41385 limclner 41395 limsupre3uzlem 41479 climuzlem 41487 xlimmnfv 41578 xlimpnfv 41582 itgperiod 41728 stoweidlem53 41801 stoweidlem57 41805 fourierdlem48 41902 fourierdlem51 41905 fourierdlem73 41927 fourierdlem81 41935 elaa2 41982 etransclem32 42014 sge0iunmptlemre 42160 voliunsge0lem 42217 meaiuninc3v 42229 isomenndlem 42275 ovnsubaddlem1 42315 hoidmvlelem1 42340 hoidmvlelem5 42344 smfaddlem1 42502 2reu7 42748 2reu8 42749 f1oresf1o2 42928 mogoldbb 43350 2zrngagrp 43610 2zrngmmgm 43613 |
Copyright terms: Public domain | W3C validator |