|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > nrex | Structured version Visualization version GIF version | ||
| Description: Inference adding restricted existential quantifier to negated wff. (Contributed by NM, 16-Oct-2003.) | 
| Ref | Expression | 
|---|---|
| nrex.1 | ⊢ (𝑥 ∈ 𝐴 → ¬ 𝜓) | 
| Ref | Expression | 
|---|---|
| nrex | ⊢ ¬ ∃𝑥 ∈ 𝐴 𝜓 | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | nrex.1 | . . 3 ⊢ (𝑥 ∈ 𝐴 → ¬ 𝜓) | |
| 2 | 1 | rgen 3063 | . 2 ⊢ ∀𝑥 ∈ 𝐴 ¬ 𝜓 | 
| 3 | ralnex 3072 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜓 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜓) | |
| 4 | 2, 3 | mpbi 230 | 1 ⊢ ¬ ∃𝑥 ∈ 𝐴 𝜓 | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 → wi 4 ∈ wcel 2108 ∀wral 3061 ∃wrex 3070 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-ral 3062 df-rex 3071 | 
| This theorem is referenced by: rex0 4360 iun0 5062 canth 7385 orduninsuc 7864 wfrlem16OLD 8364 wofib 9585 cfsuc 10297 nominpos 12503 nnunb 12522 indstr 12958 eirr 16241 sqrt2irr 16285 vdwap0 17014 smndex1n0mnd 18925 smndex2dnrinv 18928 psgnunilem3 19514 bwth 23418 zfbas 23904 aaliou3lem9 26392 vma1 27209 muls01 28138 mulsrid 28139 onmulscl 28287 hatomistici 32381 esumrnmpt2 34069 fmlan0 35396 linedegen 36144 limsucncmpi 36446 elpadd0 39811 rexanuz2nf 45503 fourierdlem62 46183 etransc 46298 0nodd 48086 2nodd 48088 1neven 48154 | 
| Copyright terms: Public domain | W3C validator |