MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexlimdva Structured version   Visualization version   GIF version

Theorem rexlimdva 3215
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 20-Jan-2007.)
Hypothesis
Ref Expression
rexlimdva.1 ((𝜑𝑥𝐴) → (𝜓𝜒))
Assertion
Ref Expression
rexlimdva (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Distinct variable groups:   𝜑,𝑥   𝜒,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimdva
StepHypRef Expression
1 rexlimdva.1 . . 3 ((𝜑𝑥𝐴) → (𝜓𝜒))
21ex 399 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32rexlimdv 3214 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 2155  wrex 3093
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-ral 3097  df-rex 3098
This theorem is referenced by:  rexlimdvaa  3216  rexlimivv  3220  rexlimdvv  3221  ssexnelpss  3912  ralxfrd2  5075  otiunsndisj  5169  iunopeqop  5170  elsnxp  5885  foco2  6595  elunirn  6727  f1elima  6738  tfrlem9a  7712  seqomlem2  7776  oawordexr  7867  odi  7890  oelimcl  7911  nnawordex  7948  nnaordex  7949  oaabs  7955  oaabs2  7956  omabs  7958  ectocld  8043  onfin  8384  dif1en  8426  isfinite2  8451  isfiniteg  8453  fofinf1o  8474  elfiun  8569  suplub2  8600  supisoex  8613  ordtypelem9  8664  ordtypelem10  8665  brwdom2  8711  brwdom3  8720  rankr1ai  8902  fodomfi2  9160  infpwfien  9162  dfac12r  9247  ackbij1  9339  cff1  9359  fin23lem21  9440  isf32lem2  9455  fin1a2lem11  9511  fin1a2lem13  9513  ficard  9666  pwcfsdom  9684  gchina  9800  eltsk2g  9852  tskr1om2  9869  rankcf  9878  inatsk  9879  tskuni  9884  nqereu  10030  ltexnq  10076  1idpr  10130  suplem1pr  10153  supsrlem  10211  axpre-sup  10269  1re  10319  negfi  11250  fiminre  11251  supaddc  11269  supadd  11270  supmul1  11271  supmul  11274  suprzcl2  11991  qmulz  12004  qbtwnre  12242  ioo0  12412  ico0  12433  ioc0  12434  icc0  12435  modmuladd  12930  addmodlteq  12963  fsequb  12992  ssnn0fi  13002  hashdom  13380  ccats1alpha  13608  reuccats1lem  13697  2cshwcshw  13789  wrdl3s3  13924  s3iunsndisj  13926  shftlem  14025  rexuzre  14309  rexico  14310  caubnd  14315  limsupbnd1  14430  limsupbnd2  14431  rlim2lt  14445  rlim3  14446  lo1bdd2  14472  lo1bddrp  14473  o1lo1  14485  climuni  14500  climshftlem  14522  o1co  14534  rlimcn1  14536  climcn1  14539  o1rlimmul  14566  lo1le  14599  rlimno1  14601  isercoll  14615  caurcvg2  14625  serf0  14628  summolem2  14664  zsum  14666  fsum2dlem  14718  geomulcvg  14823  mertenslem2  14832  ntrivcvg  14844  zprod  14882  fprod2dlem  14925  dvds1lem  15210  odd2np1lem  15278  odd2np1  15279  mod2eq1n2dvds  15285  sqoddm1div8z  15292  ltoddhalfle  15299  halfleoddlt  15300  m1expo  15306  flodddiv4  15350  dvdssqim  15486  coprmdvds2  15580  divgcdcoprm0  15591  cncongr1  15593  cncongr2  15594  dvdsnprmd  15615  isprm5  15630  rpexp  15643  ncoprmlnprm  15647  pythagtriplem1  15732  iserodd  15751  pc2dvds  15794  difsqpwdvds  15802  oddprmdvds  15818  prmpwdvds  15819  4sqlem11  15870  vdwapun  15889  vdwlem2  15897  vdwlem6  15901  vdwlem8  15903  vdwlem10  15905  vdwnnlem1  15910  vdwnnlem3  15912  0ram  15935  ramub1lem2  15942  ramcl  15944  cshwsiun  16012  cshwrepswhash1  16015  firest  16292  imasvscafn  16396  imasmnd2  17526  dfgrp3lem  17712  imasgrp2  17729  issubg4  17809  gaorber  17936  orbsta  17941  pmtr3ncom  18090  psgnran  18130  odmulg  18168  odbezout  18170  gexdvdsi  18193  sylow1lem3  18210  odcau  18214  sylow2alem1  18227  sylow3lem6  18242  lsmelvalm  18261  efgrelexlemb  18358  efgredeu  18360  cyggeninv  18480  cygctb  18488  cyggexb  18495  dprdssv  18611  dprddisj2  18634  ablfacrplem  18660  pgpfac1lem2  18670  pgpfac1lem5  18674  ringinvnz1ne0  18788  ringinvnzdiv  18789  imasring  18815  dvdsrcl2  18846  dvdsrmul1  18849  lss1d  19164  lssats2  19201  lspsn  19203  lmhmima  19248  lspsneleq  19316  lpiss  19453  mplcoe5lem  19670  mpfind  19738  cply1coe0bi  19872  gsummoncoe1  19876  mpfpf1  19917  pf1mpf  19918  dvdsrzring  20033  znunit  20113  znrrg  20115  cygznlem3  20119  frgpcyg  20123  psgnghm  20127  psgndif  20150  lindfrn  20364  islinds4  20378  mat1dimelbas  20482  mat1dimcrng  20488  scmatdmat  20526  scmataddcl  20527  scmatsubcl  20528  scmatmulcl  20529  smatvscl  20535  cpmatacl  20728  cpmatinvcl  20729  pmatcollpw3fi1lem2  20799  chpscmat  20854  tgcl  20981  clsval2  21062  neindisj  21129  innei  21137  restcld  21184  restcldr  21186  ordtrest2lem  21215  cnprest  21301  lmss  21310  lmcls  21314  lmcnp  21316  isnrm3  21371  isreg2  21389  cmpcovf  21402  cncmp  21403  cmpsub  21411  1stcrest  21464  2ndcrest  21465  dis2ndc  21471  1stccnp  21473  restnlly  21493  cldllycmp  21506  locfincmp  21537  txcnpi  21619  pthaus  21649  txtube  21651  txcmplem1  21652  txcmplem2  21653  txlm  21659  xkohaus  21664  xkococnlem  21670  xkococn  21671  kqfvima  21741  kqreglem1  21752  isfild  21869  fgcl  21889  filuni  21896  isufil2  21919  ufileu  21930  uffix  21932  rnelfm  21964  fmfnfmlem2  21966  fmfnfmlem4  21968  fmfnfm  21969  fmco  21972  fclsopn  22025  ufilcmp  22043  cnpfcf  22052  alexsublem  22055  alexsubALT  22062  cldsubg  22121  ghmcnp  22125  qustgpopn  22130  tsmsgsum  22149  tsmsres  22154  tsmsxplem1  22163  tsmsxp  22165  isucn2  22290  ucnprima  22293  imasdsf1olem  22385  blssps  22436  blss  22437  blssexps  22438  blssex  22439  mopni3  22506  blcld  22517  metrest  22536  metcnp3  22552  reperflem  22828  icccmplem3  22834  xrge0tsms  22844  mulc1cncf  22915  cncfco  22917  cnheibor  22961  bndth  22964  lebnumlem3  22969  xlebnum  22971  lebnumii  22972  nmhmcn  23126  cfil3i  23273  cmetcaulem  23292  cfilres  23300  bcthlem4  23330  bcthlem5  23331  ivthlem2  23427  ivthlem3  23428  ivthicc  23433  cniccbdd  23436  ovolunlem1  23472  ovoliunlem2  23478  ovolshftlem2  23485  ovolicc2  23497  iundisj  23523  iunmbl2  23532  dyadmax  23573  opnmbllem  23576  subopnmbl  23579  volivth  23582  vitalilem2  23584  ismbf3d  23629  mbfimaopn2  23632  mbfaddlem  23635  i1fmullem  23669  mbfi1fseqlem4  23693  ellimc3  23851  dvlip  23964  dvlip2  23966  c1liplem1  23967  dvgt0lem1  23973  dvivthlem2  23980  dvne0  23982  lhop1lem  23984  lhop2  23986  lhop  23987  tdeglem4  24028  mdegnn0cl  24039  ply1divex  24104  dvdsq1p  24128  ig1peu  24139  elply2  24160  plypf1  24176  plydivex  24260  aalioulem3  24297  aalioulem5  24299  aaliou  24301  ulmshftlem  24351  ulmcau  24357  ulmss  24359  ulmbdd  24360  ulmcn  24361  radcnvlt1  24380  eflogeq  24556  efopn  24612  cxpeq  24706  angpieqvd  24766  dcubic  24781  xrlimcnp  24903  cxploglim  24912  ftalem2  25008  ftalem7  25013  isppw2  25049  dchrptlem1  25197  dchrptlem3  25199  dchrsum2  25201  lgsdchrval  25287  lgsdchr  25288  gausslemma2dlem1a  25298  lgsquadlem1  25313  2lgslem1c  25326  2lgslem3a1  25333  2lgslem3b1  25334  2lgslem3c1  25335  2lgslem3d1  25336  2lgsoddprmlem2  25342  dchrisumlem3  25388  dchrisum0fno1  25408  pntlem3  25506  pntleml  25508  ostth3  25535  brcgr  25988  brbtwn2  25993  axbtwnid  26027  axcontlem7  26058  umgrnloop  26211  usgrnloopALT  26304  uhgrspansubgrlem  26392  nbuhgr  26449  nbupgr  26450  wwlksnextprop  27044  elwspths2on  27095  erclwwlkeqlen  27156  erclwwlktr  27159  clwwlknscsh  27207  erclwwlkneqlen  27213  erclwwlkntr  27216  eleclclwwlkn  27221  hashecclwwlkn1  27222  umgrhashecclwwlk  27223  umgr3v3e3cycl  27351  cusconngr  27358  eucrctshift  27410  2pthfrgr  27453  3cyclfrgrrn1  27454  frgrregorufr  27494  frgr2wwlk1  27498  blocnilem  27981  ubthlem1  28048  ubthlem3  28050  htthlem  28096  shsel3  28496  omlsii  28584  spansncol  28749  nmopun  29195  nmcexi  29207  riesz1  29246  elpjrn  29371  cvcon3  29465  chcv1  29536  atcvatlem  29566  chirredi  29575  br8d  29741  iundisjfi  29876  xrge0tsmsd  30104  ordtrest2NEWlem  30287  lmxrge0  30317  indf1ofs  30407  esumcst  30444  esumfsup  30451  esumpcvgval  30459  measdivcstOLD  30606  eulerpartlemgh  30759  dstfrvunirn  30855  afsval  31068  erdszelem8  31497  erdszelem11  31500  erdsze2lem2  31503  connpconn  31534  sconnpi1  31538  cvmsss2  31573  cvmfolem  31578  cvmliftmolem2  31581  cvmliftlem15  31597  cvmlift2lem1  31601  cvmlift3lem4  31621  cvmlift3lem5  31622  mrsub0  31730  mrsubcn  31733  msubrn  31743  msubvrs  31774  dvdspw  31952  br8  31962  br6  31963  br4  31964  trpredtr  32044  frrlem5e  32103  nosupno  32164  nosupbday  32166  scutun12  32232  cgrtriv  32424  btwntriv2  32434  btwncomim  32435  btwnswapid  32439  btwnintr  32441  btwnexch3  32442  btwnouttr2  32444  ifscgr  32466  cgrxfr  32477  btwnxfr  32478  btwnconn3  32525  segcon2  32527  brsegle  32530  brsegle2  32531  seglecgr12im  32532  broutsideof3  32548  linethru  32575  elhf2  32597  opnregcld  32640  cldregopn  32641  neibastop2lem  32670  matunitlindflem1  33712  poimirlem16  33732  poimirlem17  33733  poimirlem19  33735  poimirlem20  33736  poimirlem24  33740  poimirlem29  33745  heicant  33751  opnmbllem0  33752  ismblfin  33757  itg2addnclem  33767  itg2addnclem3  33769  itg2gt0cn  33771  bddiblnc  33786  ftc1anclem5  33795  ftc2nc  33800  filbcmb  33841  sdclem1  33844  fdc  33846  incsequz  33849  caushft  33862  istotbnd3  33875  sstotbnd3  33880  equivbnd  33894  cntotbnd  33900  heibor1lem  33913  heibor1  33914  bfplem2  33927  divrngidl  34132  prnc  34171  prtlem10  34638  lshpdisj  34761  cvrcon3b  35051  atnle  35091  hlhgt2  35163  hl0lt1N  35164  hl2at  35179  cvrexchlem  35193  cvratlem  35195  lvolnlelpln  35359  2lplnj  35394  ispsubcl2N  35721  lautcvr  35866  dva1dim  36760  dib1dim  36940  dib1dim2  36943  diclspsn  36969  dih1dimatlem  37104  dihlatat  37112  dihatexv  37113  dihatexv2  37114  lcfrlem9  37325  lcfrlem16  37333  mapdrvallem2  37420  mapd1o  37423  elrfi  37753  isnacs3  37769  eldiophb  37816  diophrw  37818  eldioph2b  37822  diophin  37832  eldiophss  37834  rexrabdioph  37854  diophren  37873  rencldnfilem  37880  pell1234qrdich  37921  pellfundex  37946  jm2.26a  38062  jm2.27  38070  lsmfgcl  38139  kercvrlsm  38148  lmhmfgima  38149  lpirlnr  38182  hbtlem2  38189  hbtlem4  38191  hbtlem6  38194  rngunsnply  38238  restuni3  39787  suplesup  40029  uzub  40131  limsuppnfdlem  40407  limsuppnflem  40416  limsupubuz  40419  climinf3  40422  limsupre3lem  40438  limsupre3uzlem  40441  limsupvaluz2  40444  supcnvlimsup  40446  stoweidlem57  40747  stoweidlem61  40751  fourierdlem48  40844  fourierdlem49  40845  sge0le  41097  carageniuncllem2  41212  icoresmbl  41233  hspmbllem2  41317  smflimlem2  41456  smfmullem3  41476  smfinflem  41499  otiunsndisjX  41863  iccpartrn  41935  iccpartiun  41939  iccpartnel  41943  reuccatpfxs1lem  42002  reuccatpfxs1  42003  odz2prm2pw  42044  fmtnoprmfac2lem1  42047  fmtnofac2lem  42049  fmtnofac1  42051  prmdvdsfmtnof1lem2  42066  2pwp1prm  42072  mod42tp1mod8  42088  lighneallem2  42092  lighneallem3  42093  lighneallem4  42096  dfodd6  42119  dfeven4  42120  m1expevenALTV  42129  opoeALTV  42163  opeoALTV  42164  gbowpos  42216  gbowgt5  42219  gboge9  42221  nnsum4primesodd  42253  nnsum4primesoddALTV  42254  nnsum4primeseven  42257  sprsymrelf1lem  42303  copisnmnd  42371  lidldomn1  42483  uzlidlring  42491  isldepslvec2  42836  m1modmmod  42878  aacllem  43112
  Copyright terms: Public domain W3C validator