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 2918 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
2 | nfe1 2027 | . 2 ⊢ Ⅎ𝑥∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) | |
3 | 1, 2 | nfxfr 1779 | 1 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 384 ∃wex 1704 Ⅎwnf 1708 ∈ wcel 1990 ∃wrex 2913 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-10 2019 |
This theorem depends on definitions: df-bi 197 df-ex 1705 df-nf 1710 df-rex 2918 |
This theorem is referenced by: r19.29an 3077 2rmorex 3412 nfiu1 4550 reusv2lem3 4871 elsnxpOLD 5678 fsnex 6538 eusvobj2 6643 fun11iun 7126 zfregcl 8499 zfregclOLD 8501 scott0 8749 ac6c4 9303 lbzbi 11776 mreiincl 16256 lss1d 18963 neiptopnei 20936 neitr 20984 utopsnneiplem 22051 cfilucfil 22364 mptelee 25775 isch3 28098 atom1d 29212 xrofsup 29533 2sqmo 29649 locfinreflem 29907 esumc 30113 esumrnmpt2 30130 hasheuni 30147 esumcvg 30148 esumcvgre 30153 voliune 30292 volfiniune 30293 ddemeas 30299 eulerpartlemgvv 30438 bnj900 30999 bnj1189 31077 bnj1204 31080 bnj1398 31102 bnj1444 31111 bnj1445 31112 bnj1446 31113 bnj1447 31114 bnj1467 31122 bnj1518 31132 bnj1519 31133 nosupbnd2 31862 iooelexlt 33210 ptrest 33408 poimirlem26 33435 indexa 33528 filbcmb 33535 sdclem1 33539 heibor1 33609 dihglblem5 36587 suprnmpt 39355 disjinfi 39380 fvelimad 39458 upbdrech 39519 ssfiunibd 39523 infxrunb2 39584 supxrunb3 39623 iccshift 39744 iooshift 39748 islpcn 39871 limsupre 39873 limclner 39883 limsupre3uzlem 39967 climuzlem 39975 xlimmnfv 40060 xlimpnfv 40064 itgperiod 40197 stoweidlem53 40270 stoweidlem57 40274 fourierdlem48 40371 fourierdlem51 40374 fourierdlem73 40396 fourierdlem81 40404 elaa2 40451 etransclem32 40483 sge0iunmptlemre 40632 voliunsge0lem 40689 isomenndlem 40744 ovnsubaddlem1 40784 hoidmvlelem1 40809 hoidmvlelem5 40813 smfaddlem1 40971 reuan 41180 2reurex 41181 2reu4a 41189 2reu7 41191 2reu8 41192 mogoldbb 41673 2zrngagrp 41943 2zrngmmgm 41946 |
Copyright terms: Public domain | W3C validator |