![]() |
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 3175 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ¬ 𝜓) |
3 | ralnex 3201 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜓 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜓) | |
4 | 2, 3 | sylib 210 | 1 ⊢ (𝜑 → ¬ ∃𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 386 ∈ wcel 2164 ∀wral 3117 ∃wrex 3118 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1879 df-ral 3122 df-rex 3123 |
This theorem is referenced by: class2set 5056 otiunsndisj 5208 peano5 7355 onnseq 7712 oalimcl 7912 omlimcl 7930 oeeulem 7953 nneob 8004 wemappo 8730 setind 8894 cardlim 9118 cardaleph 9232 cflim2 9407 fin23lem38 9493 isf32lem5 9501 winainflem 9837 winalim2 9840 supaddc 11327 supmul1 11329 ixxub 12491 ixxlb 12492 supicclub2 12623 s3iunsndisj 14093 rlimuni 14665 rlimcld2 14693 rlimno1 14768 harmonic 14972 eirr 15314 ruclem12 15351 dvdsle 15416 prmreclem5 16002 prmreclem6 16003 vdwnnlem3 16079 frgpnabllem1 18636 ablfacrplem 18825 lbsextlem3 19528 lmmo 21562 fbasfip 22049 hauspwpwf1 22168 alexsublem 22225 tsmsfbas 22308 iccntr 23001 reconnlem2 23007 evth 23135 bcthlem5 23503 minveclem3b 23603 itg2seq 23915 dvferm1 24154 dvferm2 24156 aaliou3lem9 24511 taylthlem2 24534 vma1 25312 pntlem3 25718 ostth2lem1 25727 tglowdim1i 25820 ordtconnlem1 30511 ballotlemimin 31109 poseq 32287 nosupbnd1lem4 32391 nocvxminlem 32427 tailfb 32905 fdc 34082 heibor1lem 34149 heiborlem8 34158 atlatmstc 35393 pmap0 35839 hdmap14lem4a 37945 cmpfiiin 38103 limcrecl 40654 dirkercncflem2 41113 fourierdlem20 41136 fourierdlem42 41158 fourierdlem46 41161 fourierdlem63 41178 fourierdlem64 41179 fourierdlem65 41180 otiunsndisjX 42180 |
Copyright terms: Public domain | W3C validator |