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

Theorem rexlimdva 3060
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 449 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32rexlimdv 3059 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2030  wrex 2942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-ral 2946  df-rex 2947
This theorem is referenced by:  rexlimdvaa  3061  rexlimivv  3065  rexlimdvv  3066  ssexnelpss  3753  ralxfrdOLD  4910  ralxfrd2  4914  otiunsndisj  5009  iunopeqop  5010  elsnxp  5715  foco2  6419  foco2OLD  6420  elunirn  6549  f1elima  6560  tfrlem9a  7527  seqomlem2  7591  oawordexr  7681  odi  7704  oelimcl  7725  nnawordex  7762  nnaordex  7763  oaabs  7769  oaabs2  7770  omabs  7772  ectocld  7857  onfin  8192  dif1en  8234  isfinite2  8259  isfiniteg  8261  fofinf1o  8282  elfiun  8377  suplub2  8408  supisoex  8421  ordtypelem9  8472  ordtypelem10  8473  brwdom2  8519  brwdom3  8528  rankr1ai  8699  fodomfi2  8921  infpwfien  8923  dfac12r  9006  ackbij1  9098  cff1  9118  fin23lem21  9199  isf32lem2  9214  fin1a2lem11  9270  fin1a2lem13  9272  ficard  9425  pwcfsdom  9443  gchina  9559  eltsk2g  9611  tskr1om2  9628  rankcf  9637  inatsk  9638  tskuni  9643  nqereu  9789  ltexnq  9835  1idpr  9889  suplem1pr  9912  supsrlem  9970  axpre-sup  10028  1re  10077  negfi  11009  fiminre  11010  supaddc  11028  supadd  11029  supmul1  11030  supmul  11033  suprzcl2  11816  qmulz  11829  qbtwnre  12068  ioo0  12238  ico0  12259  ioc0  12260  icc0  12261  modmuladd  12752  addmodlteq  12785  fsequb  12814  ssnn0fi  12824  hashdom  13206  ccats1alpha  13436  reuccats1lem  13525  2cshwcshw  13617  wrdl3s3  13751  s3iunsndisj  13753  shftlem  13852  rexuzre  14136  rexico  14137  caubnd  14142  limsupbnd1  14257  limsupbnd2  14258  rlim2lt  14272  rlim3  14273  lo1bdd2  14299  lo1bddrp  14300  o1lo1  14312  climuni  14327  climshftlem  14349  o1co  14361  rlimcn1  14363  climcn1  14366  o1rlimmul  14393  lo1le  14426  rlimno1  14428  isercoll  14442  caurcvg2  14452  serf0  14455  summolem2  14491  zsum  14493  fsum2dlem  14545  geomulcvg  14651  mertenslem2  14661  ntrivcvg  14673  zprod  14711  fprod2dlem  14754  dvds1lem  15040  odd2np1lem  15111  odd2np1  15112  mod2eq1n2dvds  15118  sqoddm1div8z  15125  ltoddhalfle  15132  halfleoddlt  15133  m1expo  15139  flodddiv4  15184  dvdssqim  15320  coprmdvds2  15415  divgcdcoprm0  15426  cncongr1  15428  cncongr2  15429  dvdsnprmd  15450  isprm5  15466  rpexp  15479  ncoprmlnprm  15483  pythagtriplem1  15568  iserodd  15587  pc2dvds  15630  difsqpwdvds  15638  oddprmdvds  15654  prmpwdvds  15655  4sqlem11  15706  vdwapun  15725  vdwlem2  15733  vdwlem6  15737  vdwlem8  15739  vdwlem10  15741  vdwnnlem1  15746  vdwnnlem3  15748  0ram  15771  ramub1lem2  15778  ramcl  15780  cshwsiun  15853  cshwrepswhash1  15856  firest  16140  imasvscafn  16244  imasmnd2  17374  dfgrp3lem  17560  imasgrp2  17577  issubg4  17660  gaorber  17787  orbsta  17792  pmtr3ncom  17941  psgnran  17981  odmulg  18019  odbezout  18021  gexdvdsi  18044  sylow1lem3  18061  odcau  18065  sylow2alem1  18078  sylow3lem6  18093  lsmelvalm  18112  efgrelexlemb  18209  efgredeu  18211  cyggeninv  18331  cygctb  18339  cyggexb  18346  dprdssv  18461  dprddisj2  18484  ablfacrplem  18510  pgpfac1lem2  18520  pgpfac1lem5  18524  ringinvnz1ne0  18638  ringinvnzdiv  18639  imasring  18665  dvdsrcl2  18696  dvdsrmul1  18699  lss1d  19011  lssats2  19048  lspsn  19050  lmhmima  19095  lspsneleq  19163  lpiss  19298  mplcoe5lem  19515  mpfind  19584  cply1coe0bi  19718  gsummoncoe1  19722  mpfpf1  19763  pf1mpf  19764  dvdsrzring  19879  znunit  19960  znrrg  19962  cygznlem3  19966  frgpcyg  19970  psgnghm  19974  psgndif  19996  lindfrn  20208  islinds4  20222  mat1dimelbas  20325  mat1dimcrng  20331  scmatdmat  20369  scmataddcl  20370  scmatsubcl  20371  scmatmulcl  20372  smatvscl  20378  cpmatacl  20569  cpmatinvcl  20570  pmatcollpw3fi1lem2  20640  chpscmat  20695  tgcl  20821  clsval2  20902  neindisj  20969  innei  20977  restcld  21024  restcldr  21026  ordtrest2lem  21055  cnprest  21141  lmss  21150  lmcls  21154  lmcnp  21156  isnrm3  21211  isreg2  21229  cmpcovf  21242  cncmp  21243  cmpsub  21251  1stcrest  21304  2ndcrest  21305  dis2ndc  21311  1stccnp  21313  restnlly  21333  cldllycmp  21346  locfincmp  21377  txcnpi  21459  pthaus  21489  txtube  21491  txcmplem1  21492  txcmplem2  21493  txlm  21499  xkohaus  21504  xkococnlem  21510  xkococn  21511  kqfvima  21581  kqreglem1  21592  isfild  21709  fgcl  21729  filuni  21736  isufil2  21759  ufileu  21770  uffix  21772  rnelfm  21804  fmfnfmlem2  21806  fmfnfmlem4  21808  fmfnfm  21809  fmco  21812  fclsopn  21865  ufilcmp  21883  cnpfcf  21892  alexsublem  21895  alexsubALT  21902  cldsubg  21961  ghmcnp  21965  qustgpopn  21970  tsmsgsum  21989  tsmsres  21994  tsmsxplem1  22003  tsmsxp  22005  isucn2  22130  ucnprima  22133  imasdsf1olem  22225  blssps  22276  blss  22277  blssexps  22278  blssex  22279  mopni3  22346  blcld  22357  metrest  22376  metcnp3  22392  reperflem  22668  icccmplem3  22674  xrge0tsms  22684  mulc1cncf  22755  cncfco  22757  cnheibor  22801  bndth  22804  lebnumlem3  22809  xlebnum  22811  lebnumii  22812  nmhmcn  22966  cfil3i  23113  cmetcaulem  23132  cfilres  23140  bcthlem4  23170  bcthlem5  23171  ivthlem2  23267  ivthlem3  23268  ivthicc  23273  cniccbdd  23276  ovolunlem1  23311  ovoliunlem2  23317  ovolshftlem2  23324  ovolicc2  23336  iundisj  23362  iunmbl2  23371  dyadmax  23412  opnmbllem  23415  subopnmbl  23418  volivth  23421  vitalilem2  23423  ismbf3d  23466  mbfimaopn2  23469  mbfaddlem  23472  i1fmullem  23506  mbfi1fseqlem4  23530  ellimc3  23688  dvlip  23801  dvlip2  23803  c1liplem1  23804  dvgt0lem1  23810  dvivthlem2  23817  dvne0  23819  lhop1lem  23821  lhop2  23823  lhop  23824  tdeglem4  23865  mdegnn0cl  23876  ply1divex  23941  dvdsq1p  23965  ig1peu  23976  elply2  23997  plypf1  24013  plydivex  24097  aalioulem3  24134  aalioulem5  24136  aaliou  24138  ulmshftlem  24188  ulmcau  24194  ulmss  24196  ulmbdd  24197  ulmcn  24198  radcnvlt1  24217  eflogeq  24393  efopn  24449  cxpeq  24543  angpieqvd  24603  dcubic  24618  xrlimcnp  24740  cxploglim  24749  ftalem2  24845  ftalem7  24850  isppw2  24886  dchrptlem1  25034  dchrptlem3  25036  dchrsum2  25038  lgsdchrval  25124  lgsdchr  25125  gausslemma2dlem1a  25135  lgsquadlem1  25150  2lgslem1c  25163  2lgslem3a1  25170  2lgslem3b1  25171  2lgslem3c1  25172  2lgslem3d1  25173  2lgsoddprmlem2  25179  dchrisumlem3  25225  dchrisum0fno1  25245  pntlem3  25343  pntleml  25345  ostth3  25372  brcgr  25825  brbtwn2  25830  axbtwnid  25864  axcontlem7  25895  umgrnloop  26048  usgrnloopALT  26140  uhgrspansubgrlem  26227  nbuhgr  26284  nbupgr  26285  wwlksnextprop  26875  elwspths2on  26926  erclwwlkeqlen  26976  erclwwlktr  26979  clwwlknscsh  27027  erclwwlkneqlen  27032  erclwwlkntr  27035  eleclclwwlkn  27040  hashecclwwlkn1  27041  umgrhashecclwwlk  27042  umgr3v3e3cycl  27162  cusconngr  27169  eucrctshift  27221  2pthfrgr  27264  3cyclfrgrrn1  27265  frgrregorufr  27305  frgr2wwlk1  27309  blocnilem  27787  ubthlem1  27854  ubthlem3  27856  htthlem  27902  shsel3  28302  omlsii  28390  spansncol  28555  nmopun  29001  nmcexi  29013  riesz1  29052  elpjrn  29177  cvcon3  29271  chcv1  29342  atcvatlem  29372  chirredi  29381  br8d  29548  iundisjfi  29683  xrge0tsmsd  29913  ordtrest2NEWlem  30096  lmxrge0  30126  indf1ofs  30216  esumcst  30253  esumfsup  30260  esumpcvgval  30268  measdivcstOLD  30415  eulerpartlemgh  30568  dstfrvunirn  30664  afsval  30877  erdszelem8  31306  erdszelem11  31309  erdsze2lem2  31312  connpconn  31343  sconnpi1  31347  cvmsss2  31382  cvmfolem  31387  cvmliftmolem2  31390  cvmliftlem15  31406  cvmlift2lem1  31410  cvmlift3lem4  31430  cvmlift3lem5  31431  mrsub0  31539  mrsubcn  31542  msubrn  31552  msubvrs  31583  dvdspw  31762  br8  31772  br6  31773  br4  31774  trpredtr  31854  frrlem5e  31913  nosupno  31974  nosupbday  31976  scutun12  32042  cgrtriv  32234  btwntriv2  32244  btwncomim  32245  btwnswapid  32249  btwnintr  32251  btwnexch3  32252  btwnouttr2  32254  ifscgr  32276  cgrxfr  32287  btwnxfr  32288  btwnconn3  32335  segcon2  32337  brsegle  32340  brsegle2  32341  seglecgr12im  32342  broutsideof3  32358  linethru  32385  elhf2  32407  opnregcld  32450  cldregopn  32451  neibastop2lem  32480  matunitlindflem1  33535  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem24  33563  poimirlem29  33568  heicant  33574  opnmbllem0  33575  ismblfin  33580  itg2addnclem  33591  itg2addnclem3  33593  itg2gt0cn  33595  bddiblnc  33610  ftc1anclem5  33619  ftc2nc  33624  filbcmb  33665  sdclem1  33669  fdc  33671  incsequz  33674  caushft  33687  istotbnd3  33700  sstotbnd3  33705  equivbnd  33719  cntotbnd  33725  heibor1lem  33738  heibor1  33739  bfplem2  33752  divrngidl  33957  prnc  33996  prtlem10  34469  lshpdisj  34592  cvrcon3b  34882  atnle  34922  hlhgt2  34993  hl0lt1N  34994  hl2at  35009  cvrexchlem  35023  cvratlem  35025  lvolnlelpln  35189  2lplnj  35224  ispsubcl2N  35551  lautcvr  35696  dva1dim  36590  dib1dim  36771  dib1dim2  36774  diclspsn  36800  dih1dimatlem  36935  dihlatat  36943  dihatexv  36944  dihatexv2  36945  lcfrlem9  37156  lcfrlem16  37164  mapdrvallem2  37251  mapd1o  37254  elrfi  37574  isnacs3  37590  eldiophb  37637  diophrw  37639  eldioph2b  37643  diophin  37653  eldiophss  37655  rexrabdioph  37675  diophren  37694  rencldnfilem  37701  pell1234qrdich  37742  pellfundex  37767  jm2.26a  37884  jm2.27  37892  lsmfgcl  37961  kercvrlsm  37970  lmhmfgima  37971  lpirlnr  38004  hbtlem2  38011  hbtlem4  38013  hbtlem6  38016  rngunsnply  38060  restuni3  39615  suplesup  39868  uzub  39971  limsuppnfdlem  40251  limsuppnflem  40260  limsupubuz  40263  climinf3  40266  limsupre3lem  40282  limsupre3uzlem  40285  limsupvaluz2  40288  supcnvlimsup  40290  stoweidlem57  40592  stoweidlem61  40596  fourierdlem48  40689  fourierdlem49  40690  sge0le  40942  carageniuncllem2  41057  icoresmbl  41078  hspmbllem2  41162  smflimlem2  41301  smfmullem3  41321  smfinflem  41344  otiunsndisjX  41621  iccpartrn  41691  iccpartiun  41695  iccpartnel  41699  reuccatpfxs1lem  41758  reuccatpfxs1  41759  odz2prm2pw  41800  fmtnoprmfac2lem1  41803  fmtnofac2lem  41805  fmtnofac1  41807  prmdvdsfmtnof1lem2  41822  2pwp1prm  41828  mod42tp1mod8  41844  lighneallem2  41848  lighneallem3  41849  lighneallem4  41852  dfodd6  41875  dfeven4  41876  m1expevenALTV  41885  opoeALTV  41919  opeoALTV  41920  gbowpos  41972  gbowgt5  41975  gboge9  41977  nnsum4primesodd  42009  nnsum4primesoddALTV  42010  nnsum4primeseven  42013  tgblthelfgottOLD  42034  sprsymrelf1lem  42066  copisnmnd  42134  lidldomn1  42246  uzlidlring  42254  isldepslvec2  42599  m1modmmod  42641  aacllem  42875
  Copyright terms: Public domain W3C validator