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 2902 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
2 | nfe1 2014 | . 2 ⊢ Ⅎ𝑥∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) | |
3 | 1, 2 | nfxfr 1771 | 1 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 383 ∃wex 1695 Ⅎwnf 1699 ∈ wcel 1977 ∃wrex 2897 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-10 2006 |
This theorem depends on definitions: df-bi 196 df-ex 1696 df-nf 1701 df-rex 2902 |
This theorem is referenced by: r19.29an 3059 2rmorex 3379 nfiu1 4486 reusv2lem3 4797 elsnxpOLD 5595 fsnex 6438 eusvobj2 6542 fun11iun 7019 zfregcl 8382 zfregclOLD 8384 scott0 8632 ac6c4 9186 lbzbi 11652 mreiincl 16079 lss1d 18784 neiptopnei 20746 neitr 20794 utopsnneiplem 21861 cfilucfil 22174 mptelee 25575 isch3 27482 atom1d 28596 xrofsup 28923 2sqmo 28980 locfinreflem 29235 esumc 29440 esumrnmpt2 29457 hasheuni 29474 esumcvg 29475 esumcvgre 29480 voliune 29619 volfiniune 29620 ddemeas 29626 eulerpartlemgvv 29765 bnj900 30253 bnj1189 30331 bnj1204 30334 bnj1398 30356 bnj1444 30365 bnj1445 30366 bnj1446 30367 bnj1447 30368 bnj1467 30376 bnj1518 30386 bnj1519 30387 iooelexlt 32386 ptrest 32578 poimirlem26 32605 indexa 32698 filbcmb 32705 sdclem1 32709 heibor1 32779 dihglblem5 35605 suprnmpt 38350 disjinfi 38375 upbdrech 38460 ssfiunibd 38464 infxrunb2 38525 iccshift 38591 iooshift 38595 islpcn 38706 limsupre 38708 limclner 38718 itgperiod 38873 stoweidlem53 38946 stoweidlem57 38950 fourierdlem48 39047 fourierdlem51 39050 fourierdlem73 39072 fourierdlem81 39080 elaa2 39127 etransclem32 39159 sge0iunmptlemre 39308 voliunsge0lem 39365 isomenndlem 39420 ovnsubaddlem1 39460 hoidmvlelem1 39485 hoidmvlelem5 39489 smfaddlem1 39649 reuan 39829 2reurex 39830 2reu4a 39838 2reu7 39840 2reu8 39841 2zrngagrp 41733 2zrngmmgm 41736 |
Copyright terms: Public domain | W3C validator |