|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > nrexdv | Structured version Visualization version GIF version | ||
| Description: Deduction adding restricted existential quantifier to negated wff. (Contributed by NM, 16-Oct-2003.) (Proof shortened by Wolf Lammen, 5-Jan-2020.) | 
| Ref | Expression | 
|---|---|
| nrexdv.1 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ¬ 𝜓) | 
| Ref | Expression | 
|---|---|
| nrexdv | ⊢ (𝜑 → ¬ ∃𝑥 ∈ 𝐴 𝜓) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | nrexdv.1 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ¬ 𝜓) | |
| 2 | 1 | ralrimiva 3145 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ¬ 𝜓) | 
| 3 | ralnex 3071 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜓 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜓) | |
| 4 | 2, 3 | sylib 218 | 1 ⊢ (𝜑 → ¬ ∃𝑥 ∈ 𝐴 𝜓) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∈ wcel 2107 ∀wral 3060 ∃wrex 3069 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-ral 3061 df-rex 3070 | 
| This theorem is referenced by: class2set 5354 otiunsndisj 5524 peano5 7916 poseq 8184 frrlem14 8325 onnseq 8385 oalimcl 8599 omlimcl 8617 oeeulem 8640 nneob 8695 wemappo 9590 setind 9775 cardlim 10013 cardaleph 10130 cflim2 10304 fin23lem38 10390 isf32lem5 10398 winainflem 10734 winalim2 10737 supaddc 12236 supmul1 12238 ixxub 13409 ixxlb 13410 supicclub2 13545 s3iunsndisj 15008 rlimuni 15587 rlimcld2 15615 rlimno1 15691 harmonic 15896 eirr 16242 ruclem12 16278 dvdsle 16348 prmreclem5 16959 prmreclem6 16960 vdwnnlem3 17036 frgpnabllem1 19892 ablfacrplem 20086 lbsextlem3 21163 lmmo 23389 fbasfip 23877 hauspwpwf1 23996 alexsublem 24053 tsmsfbas 24137 iccntr 24844 reconnlem2 24850 evth 24992 bcthlem5 25363 minveclem3b 25463 itg2seq 25778 dvferm1 26024 dvferm2 26026 aaliou3lem9 26393 taylthlem2 26417 taylthlem2OLD 26418 vma1 27210 pntlem3 27654 ostth2lem1 27663 nosupbnd1lem4 27757 noinfbnd1lem4 27772 nocvxminlem 27823 tglowdim1i 28510 ssmxidllem 33502 ordtconnlem1 33924 ballotlemimin 34509 tailfb 36379 unblimceq0 36509 fdc 37753 heibor1lem 37817 heiborlem8 37826 atlatmstc 39321 pmap0 39768 hdmap14lem4a 41874 cmpfiiin 42713 limcrecl 45649 dirkercncflem2 46124 fourierdlem20 46147 fourierdlem42 46169 fourierdlem46 46172 fourierdlem63 46189 fourierdlem64 46190 fourierdlem65 46191 otiunsndisjX 47296 | 
| Copyright terms: Public domain | W3C validator |