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

Theorem rexlimdva 3153
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 414 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32rexlimdv 3151 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wcel 2107  wrex 3074
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3075
This theorem is referenced by:  rexlimdvaa  3154  rexlimivv  3197  rexlimdvv  3205  ssexnelpss  4074  ralxfrd2  5368  iunopeqop  5479  elsnxp  6244  foco2  7058  elunirn  7199  f1elima  7211  releldmdifi  7978  mpoexw  8012  xpord3pred  8085  sexp3  8086  tfrlem9a  8333  seqomlem2  8398  oawordexr  8504  odi  8527  oelimcl  8548  nnawordex  8585  nnaordex  8586  oaabs  8595  oaabs2  8596  omabs  8598  eldifsucnn  8611  coflton  8618  cofon1  8619  cofon2  8620  cofonr  8621  naddunif  8638  ectocld  8724  onfin  9175  dif1ennnALT  9222  isfinite2  9246  isfiniteg  9249  fofinf1o  9272  elfiun  9367  suplub2  9398  supisoex  9411  ordtypelem9  9463  ordtypelem10  9464  brwdom2  9510  brwdom3  9519  ttrcltr  9653  rankr1ai  9735  fodomfi2  9997  infpwfien  9999  dfac12r  10083  ackbij1  10175  cff1  10195  fin23lem21  10276  isf32lem2  10291  fin1a2lem11  10347  fin1a2lem13  10349  ficard  10502  gchina  10636  eltsk2g  10688  tskr1om2  10705  rankcf  10714  inatsk  10715  tskuni  10720  nqereu  10866  ltexnq  10912  1idpr  10966  suplem1pr  10989  supsrlem  11048  axpre-sup  11106  1re  11156  0re  11158  0cnALT  11390  negfi  12105  supaddc  12123  supadd  12124  supmul1  12125  supmul  12128  suprzcl2  12864  qmulz  12877  elpq  12901  qbtwnre  13119  ioo0  13290  ico0  13311  ioc0  13312  icc0  13313  addmodlteq  13852  fsequb  13881  hashdom  14280  ccats1alpha  14508  reuccatpfxs1lem  14635  shftlem  14954  rexuzre  15238  rexico  15239  caubnd  15244  limsupbnd1  15365  limsupbnd2  15366  rlim2lt  15380  rlim3  15381  lo1bdd2  15407  lo1bddrp  15408  o1lo1  15420  climuni  15435  climshftlem  15457  o1co  15469  rlimcn1  15471  climcn1  15475  o1rlimmul  15502  lo1le  15537  rlimno1  15539  isercoll  15553  caurcvg2  15563  serf0  15566  summolem2  15602  zsum  15604  fsum2dlem  15656  geomulcvg  15762  mertenslem2  15771  ntrivcvg  15783  zprod  15821  fprod2dlem  15864  dvds1lem  16151  dvdsexp2im  16210  odd2np1lem  16223  sqoddm1div8z  16237  ltoddhalfle  16244  halfleoddlt  16245  flodddiv4  16296  dvdssqim  16436  coprmdvds2  16531  divgcdcoprm0  16542  cncongr1  16544  cncongr2  16545  isprm5  16584  rpexp  16599  pythagtriplem1  16689  iserodd  16708  pc2dvds  16752  difsqpwdvds  16760  oddprmdvds  16776  prmpwdvds  16777  4sqlem11  16828  vdwapun  16847  vdwlem2  16855  vdwlem6  16859  vdwlem8  16861  vdwlem10  16863  vdwnnlem1  16868  vdwnnlem3  16870  0ram  16893  ramub1lem2  16900  ramcl  16902  cshwsiun  16973  cshwrepswhash1  16976  firest  17315  imasvscafn  17420  imasmnd2  18594  dfgrp3lem  18846  imasgrp2  18863  issubg4  18948  cycsubm  18996  gaorber  19089  orbsta  19094  pmtr3ncom  19258  psgnran  19298  odmulg  19339  odbezout  19341  gexdvdsi  19366  sylow1lem3  19383  odcau  19387  sylow2alem1  19400  sylow3lem6  19415  lsmelvalm  19434  efgrelexlemb  19533  efgredeu  19535  cyggeninv  19661  cygctb  19670  cyggexb  19677  dprdssv  19796  dprddisj2  19819  ablfacrplem  19845  pgpfac1lem2  19855  pgpfac1lem5  19859  ringinvnzdiv  20018  imasring  20046  dvdsrcl2  20080  dvdsrmul1  20083  lss1d  20427  lssats2  20464  lspsn  20466  lmhmima  20511  lpiss  20723  dvdsrzring  20885  znunit  20973  znrrg  20975  cygznlem3  20979  frgpcyg  20983  lindfrn  21230  mplcoe5lem  21443  mpfind  21520  gsummoncoe1  21678  mpfpf1  21720  pf1mpf  21721  mat1dimelbas  21823  scmatdmat  21867  scmataddcl  21868  scmatsubcl  21869  scmatmulcl  21870  cpmatacl  22068  chpscmat  22194  tgcl  22322  clsval2  22404  innei  22479  restcld  22526  restcldr  22528  ordtrest2lem  22557  cnprest  22643  lmss  22652  lmcls  22656  lmcnp  22658  isreg2  22731  cmpcovf  22745  cncmp  22746  cmpsub  22754  1stcrest  22807  2ndcrest  22808  1stccnp  22816  restnlly  22836  cldllycmp  22849  locfincmp  22880  txcnpi  22962  pthaus  22992  txtube  22994  txcmplem1  22995  txcmplem2  22996  txlm  23002  xkohaus  23007  xkococnlem  23013  xkococn  23014  kqfvima  23084  kqreglem1  23095  isfild  23212  filuni  23239  isufil2  23262  uffix  23275  rnelfm  23307  fmfnfmlem2  23309  fmfnfmlem4  23311  fmfnfm  23312  fmco  23315  fclsopn  23368  ufilcmp  23386  cnpfcf  23395  alexsublem  23398  alexsubALT  23405  cldsubg  23465  ghmcnp  23469  qustgpopn  23474  tsmsgsum  23493  tsmsres  23498  tsmsxplem1  23507  tsmsxp  23509  isucn2  23634  ucnprima  23637  imasdsf1olem  23729  blssps  23780  blss  23781  blssexps  23782  blssex  23783  mopni3  23853  blcld  23864  metrest  23883  metcnp3  23899  reperflem  24184  icccmplem3  24190  xrge0tsms  24200  mulc1cncf  24271  cncfco  24273  cnheibor  24321  bndth  24324  lebnumlem3  24329  xlebnum  24331  lebnumii  24332  nmhmcn  24486  cfil3i  24636  cmetcaulem  24655  cfilres  24663  bcthlem4  24694  ivthlem2  24819  ivthlem3  24820  ivthicc  24825  cniccbdd  24828  ovolunlem1  24864  ovoliunlem2  24870  ovolshftlem2  24877  ovolicc2  24889  iunmbl2  24924  dyadmax  24965  opnmbllem  24968  subopnmbl  24971  volivth  24974  ismbf3d  25021  mbfimaopn2  25024  mbfaddlem  25027  i1fmullem  25061  mbfi1fseqlem4  25086  bddiblnc  25209  ellimc3  25246  dvlip  25360  dvlip2  25362  c1liplem1  25363  dvgt0lem1  25369  dvivthlem2  25376  dvne0  25378  lhop1lem  25380  lhop2  25382  lhop  25383  tdeglem4  25427  tdeglem4OLD  25428  mdegnn0cl  25439  ply1divex  25504  dvdsq1p  25528  ig1peu  25539  elply2  25560  plypf1  25576  plydivex  25660  aalioulem3  25697  aalioulem5  25699  aaliou  25701  ulmshftlem  25751  ulmcau  25757  ulmss  25759  ulmbdd  25760  ulmcn  25761  radcnvlt1  25780  eflogeq  25960  efopn  26016  cxpeq  26113  angpieqvd  26184  xrlimcnp  26321  cxploglim  26330  ftalem2  26426  ftalem7  26431  isppw2  26467  dchrptlem1  26615  dchrptlem3  26617  dchrsum2  26619  lgsdchrval  26705  lgsdchr  26706  gausslemma2dlem1a  26716  lgsquadlem1  26731  2lgsoddprmlem2  26760  dchrisumlem3  26842  dchrisum0fno1  26862  pntlem3  26960  pntleml  26962  ostth3  26989  nosupno  27054  nosupbday  27056  noinfbday  27071  scutun12  27152  oldssmade  27210  addsproplem2  27285  addsunif  27313  negsid  27342  negsunif  27353  brcgr  27852  brbtwn2  27857  axbtwnid  27891  axcontlem7  27922  usgrnloopALT  28154  uhgrspansubgrlem  28241  nbuhgr  28294  nbupgr  28295  wwlksnextprop  28860  elwspths2on  28908  erclwwlktr  28969  clwwlknscsh  29009  erclwwlkntr  29018  hashecclwwlkn1  29024  umgrhashecclwwlk  29025  3cyclfrgrrn1  29232  frgrregorufr  29272  frgr2wwlk1  29276  ubthlem1  29815  ubthlem3  29817  htthlem  29862  omlsii  30348  spansncol  30513  nmopun  30959  nmcexi  30971  riesz1  31010  elpjrn  31135  cvcon3  31229  chcv1  31300  atcvatlem  31330  chirredi  31339  br8d  31532  xrge0tsmsd  31902  ordtrest2NEWlem  32506  lmxrge0  32536  esumfsup  32672  esumpcvgval  32680  measdivcstALTV  32827  eulerpartlemgh  32981  dstfrvunirn  33077  afsval  33287  erdszelem8  33795  erdszelem11  33798  erdsze2lem2  33801  connpconn  33832  sconnpi1  33836  cvmsss2  33871  cvmfolem  33876  cvmliftmolem2  33879  cvmliftlem15  33895  cvmlift2lem1  33899  cvmlift3lem4  33919  cvmlift3lem5  33920  satfdmlem  33965  fmla1  33984  gonarlem  33991  gonar  33992  goalrlem  33993  goalr  33994  fmla0disjsuc  33995  fmlasucdisj  33996  satffunlem1lem1  33999  satffunlem1lem2  34000  satffunlem2lem1  34001  mrsub0  34113  mrsubcn  34116  msubrn  34126  msubvrs  34157  br8  34332  br6  34333  br4  34334  cgrtriv  34590  btwntriv2  34600  btwncomim  34601  btwnswapid  34605  btwnintr  34607  btwnexch3  34608  btwnouttr2  34610  ifscgr  34632  cgrxfr  34643  btwnxfr  34644  btwnconn3  34691  segcon2  34693  brsegle  34696  seglecgr12im  34698  broutsideof3  34714  linethru  34741  elhf2  34763  opnregcld  34805  cldregopn  34806  neibastop2lem  34835  matunitlindflem1  36077  poimirlem16  36097  poimirlem17  36098  poimirlem19  36100  poimirlem20  36101  poimirlem24  36105  poimirlem29  36110  heicant  36116  opnmbllem0  36117  ismblfin  36122  itg2addnclem  36132  itg2addnclem3  36134  itg2gt0cn  36136  ftc1anclem5  36158  ftc2nc  36163  filbcmb  36202  fdc  36207  incsequz  36210  caushft  36223  istotbnd3  36233  equivbnd  36252  cntotbnd  36258  heibor1lem  36271  heibor1  36272  bfplem2  36285  divrngidl  36490  prnc  36529  lshpdisj  37452  cvrcon3b  37742  atnle  37782  hlhgt2  37855  hl0lt1N  37856  hl2at  37871  cvrexchlem  37885  cvratlem  37887  lvolnlelpln  38051  2lplnj  38086  ispsubcl2N  38413  lautcvr  38558  dva1dim  39451  dib1dim  39631  dib1dim2  39634  diclspsn  39660  dih1dimatlem  39795  dihlatat  39803  dihatexv  39804  dihatexv2  39805  lcfrlem9  40016  lcfrlem16  40024  mapdrvallem2  40111  mapd1o  40114  elre0re  40780  dvdsexpim  40817  prjspner1  40967  dffltz  40975  rexlimdv3d  41009  elrfi  41020  isnacs3  41036  eldiophb  41083  eldiophss  41100  diophren  41139  rencldnfilem  41146  pell1234qrdich  41187  pellfundex  41212  lsmfgcl  41404  kercvrlsm  41413  lmhmfgima  41414  lpirlnr  41447  hbtlem2  41454  hbtlem4  41456  hbtlem6  41459  rngunsnply  41503  onexoegt  41581  cantnfresb  41661  omabs2  41668  restuni3  43335  limsupubuz  43961  stoweidlem57  44305  fourierdlem48  44402  fourierdlem49  44403  sge0le  44655  fsetsniunop  45290  cfsetsnfsetfo  45301  fcoresf1  45310  euoreqb  45348  imasetpreimafvbijlemf1  45603  imasetpreimafvbijlemfo  45604  iccpartrn  45629  iccpartiun  45633  iccpartnel  45637  paireqne  45710  reupr  45721  odz2prm2pw  45762  fmtnofac2lem  45767  prmdvdsfmtnof1lem2  45784  2pwp1prm  45788  mod42tp1mod8  45801  lighneallem3  45806  lighneallem4  45809  requad01  45820  requad2  45822  fppr2odd  45930  gbowpos  45958  gbowgt5  45961  gboge9  45963  nnsum4primesodd  45995  nnsum4primesoddALTV  45996  isomushgr  46025  isomuspgrlem2d  46030  copisnmnd  46110  lidldomn1  46226  affinecomb1  46795  eenglngeehlnmlem2  46831  rrx2vlinest  46834  itsclquadb  46869  rspceb2dv  46895  aacllem  47255
  Copyright terms: Public domain W3C validator