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

Theorem rexlimdva 3284
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 413 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32rexlimdv 3283 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2105  wrex 3139
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-ral 3143  df-rex 3144
This theorem is referenced by:  rexlimdvaa  3285  rexlimivv  3292  rexlimdvv  3293  ssexnelpss  4089  ralxfrd2  5304  iunopeqop  5403  elsnxp  6136  foco2  6866  elunirn  7001  f1elima  7012  releldmdifi  7735  mpoexw  7767  tfrlem9a  8013  seqomlem2  8078  oawordexr  8172  odi  8195  oelimcl  8216  nnawordex  8253  nnaordex  8254  oaabs  8261  oaabs2  8262  omabs  8264  ectocld  8354  onfin  8698  dif1en  8740  isfinite2  8765  isfiniteg  8767  fofinf1o  8788  elfiun  8883  suplub2  8914  supisoex  8927  ordtypelem9  8979  ordtypelem10  8980  brwdom2  9026  brwdom3  9035  rankr1ai  9216  fodomfi2  9475  infpwfien  9477  dfac12r  9561  ackbij1  9649  cff1  9669  fin23lem21  9750  isf32lem2  9765  fin1a2lem11  9821  fin1a2lem13  9823  ficard  9976  gchina  10110  eltsk2g  10162  tskr1om2  10179  rankcf  10188  inatsk  10189  tskuni  10194  nqereu  10340  ltexnq  10386  1idpr  10440  suplem1pr  10463  supsrlem  10522  axpre-sup  10580  1re  10630  0re  10632  0cnALT  10863  negfi  11578  fiminreOLD  11579  supaddc  11597  supadd  11598  supmul1  11599  supmul  11602  suprzcl2  12327  qmulz  12340  elpq  12364  qbtwnre  12582  ioo0  12753  ico0  12774  ioc0  12775  icc0  12776  addmodlteq  13304  fsequb  13333  hashdom  13730  ccats1alpha  13963  reuccatpfxs1lem  14098  shftlem  14417  rexuzre  14702  rexico  14703  caubnd  14708  limsupbnd1  14829  limsupbnd2  14830  rlim2lt  14844  rlim3  14845  lo1bdd2  14871  lo1bddrp  14872  o1lo1  14884  climuni  14899  climshftlem  14921  o1co  14933  rlimcn1  14935  climcn1  14938  o1rlimmul  14965  lo1le  14998  rlimno1  15000  isercoll  15014  caurcvg2  15024  serf0  15027  summolem2  15063  zsum  15065  fsum2dlem  15115  geomulcvg  15222  mertenslem2  15231  ntrivcvg  15243  zprod  15281  fprod2dlem  15324  dvds1lem  15611  odd2np1lem  15679  sqoddm1div8z  15693  ltoddhalfle  15700  halfleoddlt  15701  flodddiv4  15754  dvdssqim  15894  coprmdvds2  15988  divgcdcoprm0  15999  cncongr1  16001  cncongr2  16002  isprm5  16041  rpexp  16054  pythagtriplem1  16143  iserodd  16162  pc2dvds  16205  difsqpwdvds  16213  oddprmdvds  16229  prmpwdvds  16230  4sqlem11  16281  vdwapun  16300  vdwlem2  16308  vdwlem6  16312  vdwlem8  16314  vdwlem10  16316  vdwnnlem1  16321  vdwnnlem3  16323  0ram  16346  ramub1lem2  16353  ramcl  16355  cshwsiun  16423  cshwrepswhash1  16426  firest  16696  imasvscafn  16800  imasmnd2  17938  dfgrp3lem  18137  imasgrp2  18154  issubg4  18238  cycsubm  18285  gaorber  18378  orbsta  18383  pmtr3ncom  18534  psgnran  18574  odmulg  18614  odbezout  18616  gexdvdsi  18639  sylow1lem3  18656  odcau  18660  sylow2alem1  18673  sylow3lem6  18688  lsmelvalm  18707  efgrelexlemb  18807  efgredeu  18809  cyggeninv  18933  cygctb  18943  cyggexb  18950  dprdssv  19069  dprddisj2  19092  ablfacrplem  19118  pgpfac1lem2  19128  pgpfac1lem5  19132  ringinvnzdiv  19274  imasring  19300  dvdsrcl2  19331  dvdsrmul1  19334  lss1d  19666  lssats2  19703  lspsn  19705  lmhmima  19750  lpiss  19953  mplcoe5lem  20178  mpfind  20250  gsummoncoe1  20402  mpfpf1  20444  pf1mpf  20445  dvdsrzring  20560  znunit  20640  znrrg  20642  cygznlem3  20646  frgpcyg  20650  lindfrn  20895  mat1dimelbas  21010  scmatdmat  21054  scmataddcl  21055  scmatsubcl  21056  scmatmulcl  21057  cpmatacl  21254  chpscmat  21380  tgcl  21507  clsval2  21588  innei  21663  restcld  21710  restcldr  21712  ordtrest2lem  21741  cnprest  21827  lmss  21836  lmcls  21840  lmcnp  21842  isreg2  21915  cmpcovf  21929  cncmp  21930  cmpsub  21938  1stcrest  21991  2ndcrest  21992  1stccnp  22000  restnlly  22020  cldllycmp  22033  locfincmp  22064  txcnpi  22146  pthaus  22176  txtube  22178  txcmplem1  22179  txcmplem2  22180  txlm  22186  xkohaus  22191  xkococnlem  22197  xkococn  22198  kqfvima  22268  kqreglem1  22279  isfild  22396  filuni  22423  isufil2  22446  uffix  22459  rnelfm  22491  fmfnfmlem2  22493  fmfnfmlem4  22495  fmfnfm  22496  fmco  22499  fclsopn  22552  ufilcmp  22570  cnpfcf  22579  alexsublem  22582  alexsubALT  22589  cldsubg  22648  ghmcnp  22652  qustgpopn  22657  tsmsgsum  22676  tsmsres  22681  tsmsxplem1  22690  tsmsxp  22692  isucn2  22817  ucnprima  22820  imasdsf1olem  22912  blssps  22963  blss  22964  blssexps  22965  blssex  22966  mopni3  23033  blcld  23044  metrest  23063  metcnp3  23079  reperflem  23355  icccmplem3  23361  xrge0tsms  23371  mulc1cncf  23442  cncfco  23444  cnheibor  23488  bndth  23491  lebnumlem3  23496  xlebnum  23498  lebnumii  23499  nmhmcn  23653  cfil3i  23801  cmetcaulem  23820  cfilres  23828  bcthlem4  23859  ivthlem2  23982  ivthlem3  23983  ivthicc  23988  cniccbdd  23991  ovolunlem1  24027  ovoliunlem2  24033  ovolshftlem2  24040  ovolicc2  24052  iunmbl2  24087  dyadmax  24128  opnmbllem  24131  subopnmbl  24134  volivth  24137  ismbf3d  24184  mbfimaopn2  24187  mbfaddlem  24190  i1fmullem  24224  mbfi1fseqlem4  24248  ellimc3  24406  dvlip  24519  dvlip2  24521  c1liplem1  24522  dvgt0lem1  24528  dvivthlem2  24535  dvne0  24537  lhop1lem  24539  lhop2  24541  lhop  24542  tdeglem4  24583  mdegnn0cl  24594  ply1divex  24659  dvdsq1p  24683  ig1peu  24694  elply2  24715  plypf1  24731  plydivex  24815  aalioulem3  24852  aalioulem5  24854  aaliou  24856  ulmshftlem  24906  ulmcau  24912  ulmss  24914  ulmbdd  24915  ulmcn  24916  radcnvlt1  24935  eflogeq  25112  efopn  25168  cxpeq  25265  angpieqvd  25336  xrlimcnp  25474  cxploglim  25483  ftalem2  25579  ftalem7  25584  isppw2  25620  dchrptlem1  25768  dchrptlem3  25770  dchrsum2  25772  lgsdchrval  25858  lgsdchr  25859  gausslemma2dlem1a  25869  lgsquadlem1  25884  2lgsoddprmlem2  25913  dchrisumlem3  25995  dchrisum0fno1  26015  pntlem3  26113  pntleml  26115  ostth3  26142  brcgr  26614  brbtwn2  26619  axbtwnid  26653  axcontlem7  26684  usgrnloopALT  26913  uhgrspansubgrlem  27000  nbuhgr  27053  nbupgr  27054  wwlksnextprop  27619  elwspths2on  27667  erclwwlktr  27728  clwwlknscsh  27769  erclwwlkntr  27778  hashecclwwlkn1  27784  umgrhashecclwwlk  27785  3cyclfrgrrn1  27992  frgrregorufr  28032  frgr2wwlk1  28036  ubthlem1  28575  ubthlem3  28577  htthlem  28622  omlsii  29108  spansncol  29273  nmopun  29719  nmcexi  29731  riesz1  29770  elpjrn  29895  cvcon3  29989  chcv1  30060  atcvatlem  30090  chirredi  30099  br8d  30290  xrge0tsmsd  30620  ordtrest2NEWlem  31065  lmxrge0  31095  esumfsup  31229  esumpcvgval  31237  measdivcstALTV  31384  eulerpartlemgh  31536  dstfrvunirn  31632  afsval  31842  erdszelem8  32343  erdszelem11  32346  erdsze2lem2  32349  connpconn  32380  sconnpi1  32384  cvmsss2  32419  cvmfolem  32424  cvmliftmolem2  32427  cvmliftlem15  32443  cvmlift2lem1  32447  cvmlift3lem4  32467  cvmlift3lem5  32468  satfdmlem  32513  fmla1  32532  gonarlem  32539  gonar  32540  goalrlem  32541  goalr  32542  fmla0disjsuc  32543  fmlasucdisj  32544  satffunlem1lem1  32547  satffunlem1lem2  32548  satffunlem2lem1  32549  mrsub0  32661  mrsubcn  32664  msubrn  32674  msubvrs  32705  dvdspw  32880  br8  32890  br6  32891  br4  32892  nosupno  33101  nosupbday  33103  scutun12  33169  cgrtriv  33361  btwntriv2  33371  btwncomim  33372  btwnswapid  33376  btwnintr  33378  btwnexch3  33379  btwnouttr2  33381  ifscgr  33403  cgrxfr  33414  btwnxfr  33415  btwnconn3  33462  segcon2  33464  brsegle  33467  seglecgr12im  33469  broutsideof3  33485  linethru  33512  elhf2  33534  opnregcld  33576  cldregopn  33577  neibastop2lem  33606  matunitlindflem1  34770  poimirlem16  34790  poimirlem17  34791  poimirlem19  34793  poimirlem20  34794  poimirlem24  34798  poimirlem29  34803  heicant  34809  opnmbllem0  34810  ismblfin  34815  itg2addnclem  34825  itg2addnclem3  34827  itg2gt0cn  34829  bddiblnc  34844  ftc1anclem5  34853  ftc2nc  34858  filbcmb  34898  fdc  34903  incsequz  34906  caushft  34919  istotbnd3  34932  equivbnd  34951  cntotbnd  34957  heibor1lem  34970  heibor1  34971  bfplem2  34984  divrngidl  35189  prnc  35228  lshpdisj  36005  cvrcon3b  36295  atnle  36335  hlhgt2  36407  hl0lt1N  36408  hl2at  36423  cvrexchlem  36437  cvratlem  36439  lvolnlelpln  36603  2lplnj  36638  ispsubcl2N  36965  lautcvr  37110  dva1dim  38003  dib1dim  38183  dib1dim2  38186  diclspsn  38212  dih1dimatlem  38347  dihlatat  38355  dihatexv  38356  dihatexv2  38357  lcfrlem9  38568  lcfrlem16  38576  mapdrvallem2  38663  mapd1o  38666  elre0re  39034  dvdsexpim  39061  dffltz  39151  rexlimdv3d  39160  elrfi  39171  isnacs3  39187  eldiophb  39234  eldiophss  39251  diophren  39290  rencldnfilem  39297  pell1234qrdich  39338  pellfundex  39363  lsmfgcl  39554  kercvrlsm  39563  lmhmfgima  39564  lpirlnr  39597  hbtlem2  39604  hbtlem4  39606  hbtlem6  39609  rngunsnply  39653  restuni3  41265  limsupubuz  41874  stoweidlem57  42223  fourierdlem48  42320  fourierdlem49  42321  sge0le  42570  euoreqb  43189  iccpartrn  43437  iccpartiun  43441  iccpartnel  43445  paireqne  43520  reupr  43531  odz2prm2pw  43572  fmtnofac2lem  43577  prmdvdsfmtnof1lem2  43594  2pwp1prm  43598  mod42tp1mod8  43614  lighneallem3  43619  lighneallem4  43622  requad01  43633  requad2  43635  fppr2odd  43743  gbowpos  43771  gbowgt5  43774  gboge9  43776  nnsum4primesodd  43808  nnsum4primesoddALTV  43809  isomushgr  43838  isomuspgrlem2d  43843  copisnmnd  43923  lidldomn1  44090  affinecomb1  44587  eenglngeehlnmlem2  44623  rrx2vlinest  44626  itsclquadb  44661  aacllem  44800
  Copyright terms: Public domain W3C validator