![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nrexdv | Structured version Visualization version Unicode 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 2809 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | ralnex 2834 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | sylib 201 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 |
This theorem depends on definitions: df-bi 190 df-an 378 df-ex 1672 df-ral 2761 df-rex 2762 |
This theorem is referenced by: class2set 4568 otiunsndisj 4707 peano5 6735 onnseq 7081 oalimcl 7279 omlimcl 7297 oeeulem 7320 nneob 7371 wemappo 8082 setind 8236 cardlim 8424 cardaleph 8538 cflim2 8711 fin23lem38 8797 isf32lem5 8805 winainflem 9136 winalim2 9139 supaddc 10596 supmul1 10598 ixxub 11681 ixxlb 11682 ixxlbOLD 11683 supicclub2 11809 rlimuni 13691 rlimcld2 13719 rlimno1 13794 harmonic 13994 eirr 14334 ruclem12 14370 dvdsle 14427 prmreclem5 14943 prmreclem6 14944 vdwnnlem3 15026 frgpnabllem1 17587 ablfacrplem 17776 lbsextlem3 18461 lmmo 20473 fbasfip 20961 hauspwpwf1 21080 alexsublem 21137 tsmsfbas 21220 iccntr 21917 reconnlem2 21923 evth 22065 bcthlem5 22374 minveclem3b 22448 minveclem3bOLD 22460 itg2seq 22779 dvferm1 23016 dvferm2 23018 aaliou3lem9 23385 taylthlem2 23408 vma1 24172 pntlem3 24526 ostth2lem1 24535 tglowdim1i 24624 2spotiundisj 25869 2spot0 25871 ordtconlem1 28804 ballotlemimin 29411 ballotlemiminOLD 29449 poseq 30562 nocvxminlem 30650 tailfb 31104 fdc 32138 heibor1lem 32205 heiborlem8 32214 atlatmstc 32956 pmap0 33401 hdmap14lem4a 35513 cmpfiiin 35610 limcrecl 37806 dirkercncflem2 38078 fourierdlem20 38101 fourierdlem42 38124 fourierdlem42OLD 38125 fourierdlem46 38128 fourierdlem63 38145 fourierdlem64 38146 fourierdlem65 38147 otiunsndisjX 39152 |
Copyright terms: Public domain | W3C validator |