![]() |
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 3138 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ¬ 𝜓) |
3 | ralnex 3064 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜓 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜓) | |
4 | 2, 3 | sylib 217 | 1 ⊢ (𝜑 → ¬ ∃𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∈ wcel 2098 ∀wral 3053 ∃wrex 3062 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1774 df-ral 3054 df-rex 3063 |
This theorem is referenced by: class2set 5343 otiunsndisj 5510 peano5 7877 peano5OLD 7878 poseq 8138 frrlem14 8279 onnseq 8339 oalimcl 8555 omlimcl 8573 oeeulem 8596 nneob 8651 wemappo 9540 setind 9725 cardlim 9963 cardaleph 10080 cflim2 10254 fin23lem38 10340 isf32lem5 10348 winainflem 10684 winalim2 10687 supaddc 12178 supmul1 12180 ixxub 13342 ixxlb 13343 supicclub2 13478 s3iunsndisj 14912 rlimuni 15491 rlimcld2 15519 rlimno1 15597 harmonic 15802 eirr 16145 ruclem12 16181 dvdsle 16250 prmreclem5 16852 prmreclem6 16853 vdwnnlem3 16929 frgpnabllem1 19783 ablfacrplem 19977 lbsextlem3 21001 lmmo 23206 fbasfip 23694 hauspwpwf1 23813 alexsublem 23870 tsmsfbas 23954 iccntr 24659 reconnlem2 24665 evth 24807 bcthlem5 25178 minveclem3b 25278 itg2seq 25594 dvferm1 25839 dvferm2 25841 aaliou3lem9 26204 taylthlem2 26227 vma1 27014 pntlem3 27458 ostth2lem1 27467 nosupbnd1lem4 27560 noinfbnd1lem4 27575 nocvxminlem 27626 tglowdim1i 28221 ssmxidllem 33058 ordtconnlem1 33393 ballotlemimin 33993 gg-taylthlem2 35657 tailfb 35752 unblimceq0 35873 fdc 37103 heibor1lem 37167 heiborlem8 37176 atlatmstc 38679 pmap0 39126 hdmap14lem4a 41232 cmpfiiin 41924 limcrecl 44830 dirkercncflem2 45305 fourierdlem20 45328 fourierdlem42 45350 fourierdlem46 45353 fourierdlem63 45370 fourierdlem64 45371 fourierdlem65 45372 otiunsndisjX 46472 |
Copyright terms: Public domain | W3C validator |