Theorem rexlimdva 3134

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

Step	Hyp	Ref	Expression
1		rexlimdva.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
2	1	ex 412	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	rexlimdv 3132	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3054

This theorem is referenced by:  rexlimdvaa  3135  rexlimivv  3179  rexlimdvv  3193  rspceb2dv  3592  ssexnelpss  4079  ralxfrd2  5367  iunopeqop  5481  elsnxp  6264  foco2  7081  elunirn  7225  f1elima  7238  mptcnfimad  7965  releldmdifi  8024  mpoexw  8057  xpord3pred  8131  sexp3  8132  tfrlem9a  8354  seqomlem2  8419  oawordexr  8520  odi  8543  oelimcl  8564  nnawordex  8601  nnaordex  8602  oaabs  8612  oaabs2  8613  omabs  8615  eldifsucnn  8628  coflton  8635  cofon1  8636  cofon2  8637  cofonr  8638  naddunif  8657  ectocld  8755  onfin  9179  dif1ennnALT  9222  isfinite2  9245  isfiniteg  9248  fofinf1o  9283  elfiun  9381  suplub2  9412  supisoex  9426  ordtypelem9  9479  ordtypelem10  9480  brwdom2  9526  brwdom3  9535  ttrcltr  9669  rankr1ai  9751  fodomfi2  10013  infpwfien  10015  dfac12r  10100  ackbij1  10190  cff1  10211  fin23lem21  10292  isf32lem2  10307  fin1a2lem11  10363  fin1a2lem13  10365  ficard  10518  gchina  10652  eltsk2g  10704  tskr1om2  10721  rankcf  10730  inatsk  10731  tskuni  10736  nqereu  10882  ltexnq  10928  1idpr  10982  suplem1pr  11005  supsrlem  11064  axpre-sup  11122  1re  11174  0re  11176  0cnALT  11409  supaddc  12150  supadd  12151  supmul1  12152  supmul  12155  suprzcl2  12897  qmulz  12910  elpq  12934  qbtwnre  13159  ioo0  13331  ico0  13352  ioc0  13353  icc0  13354  addmodlteq  13911  fsequb  13940  hashdom  14344  ccats1alpha  14584  reuccatpfxs1lem  14711  shftlem  15034  rexuzre  15319  rexico  15320  caubnd  15325  limsupbnd1  15448  limsupbnd2  15449  rlim2lt  15463  rlim3  15464  lo1bdd2  15490  lo1bddrp  15491  o1lo1  15503  climuni  15518  climshftlem  15540  o1co  15552  rlimcn1  15554  climcn1  15558  o1rlimmul  15585  lo1le  15618  rlimno1  15620  isercoll  15634  caurcvg2  15644  serf0  15647  summolem2  15682  zsum  15684  fsum2dlem  15736  geomulcvg  15842  mertenslem2  15851  ntrivcvg  15863  zprod  15903  fprod2dlem  15946  dvds1lem  16237  dvdsexp2im  16297  odd2np1lem  16310  sqoddm1div8z  16324  ltoddhalfle  16331  halfleoddlt  16332  flodddiv4  16385  dvdssqim  16524  dvdsexpim  16525  coprmdvds2  16624  divgcdcoprm0  16635  cncongr1  16637  cncongr2  16638  isprm5  16677  rpexp  16692  pythagtriplem1  16787  iserodd  16806  pc2dvds  16850  difsqpwdvds  16858  oddprmdvds  16874  prmpwdvds  16875  4sqlem11  16926  vdwapun  16945  vdwlem2  16953  vdwlem6  16957  vdwlem8  16959  vdwlem10  16961  vdwnnlem1  16966  vdwnnlem3  16968  0ram  16991  ramub1lem2  16998  ramcl  17000  cshwsiun  17070  cshwrepswhash1  17073  firest  17395  imasvscafn  17500  imasmnd2  18701  dfgrp3lem  18970  imasgrp2  18987  issubg4  19077  cycsubm  19134  gaorber  19240  orbsta  19245  pmtr3ncom  19405  psgnran  19445  odmulg  19486  odbezout  19488  gexdvdsi  19513  sylow1lem3  19530  odcau  19534  sylow2alem1  19547  sylow3lem6  19562  lsmelvalm  19581  efgrelexlemb  19680  efgredeu  19682  imasabl  19806  cyggeninv  19813  cygctb  19822  cyggexb  19829  dprdssv  19948  dprddisj2  19971  ablfacrplem  19997  pgpfac1lem2  20007  pgpfac1lem5  20011  ringinvnzdiv  20210  imasring  20239  dvdsrcl2  20275  dvdsrmul1  20278  lss1d  20869  lssats2  20906  lspsn  20908  lmhmima  20954  ring2idlqusb  21220  rngqiprngfulem2  21222  lpiss  21239  dvdsrzring  21371  pzriprnglem5  21395  pzriprnglem8  21398  pzriprnglem10  21400  pzriprnglem11  21401  znunit  21473  znrrg  21475  cygznlem3  21479  frgpcyg  21483  lindfrn  21730  mplcoe5lem  21946  mpfind  22014  gsummoncoe1  22195  mpfpf1  22238  pf1mpf  22239  mat1dimelbas  22358  scmatdmat  22402  scmataddcl  22403  scmatsubcl  22404  scmatmulcl  22405  cpmatacl  22603  chpscmat  22729  tgcl  22856  clsval2  22937  innei  23012  restcld  23059  restcldr  23061  ordtrest2lem  23090  cnprest  23176  lmss  23185  lmcls  23189  lmcnp  23191  isreg2  23264  cmpcovf  23278  cncmp  23279  cmpsub  23287  1stcrest  23340  2ndcrest  23341  1stccnp  23349  restnlly  23369  cldllycmp  23382  locfincmp  23413  txcnpi  23495  pthaus  23525  txtube  23527  txcmplem1  23528  txcmplem2  23529  txlm  23535  xkohaus  23540  xkococnlem  23546  xkococn  23547  kqfvima  23617  kqreglem1  23628  isfild  23745  filuni  23772  isufil2  23795  uffix  23808  rnelfm  23840  fmfnfmlem2  23842  fmfnfmlem4  23844  fmfnfm  23845  fmco  23848  fclsopn  23901  ufilcmp  23919  cnpfcf  23928  alexsublem  23931  alexsubALT  23938  cldsubg  23998  ghmcnp  24002  qustgpopn  24007  tsmsgsum  24026  tsmsres  24031  tsmsxplem1  24040  tsmsxp  24042  isucn2  24166  ucnprima  24169  imasdsf1olem  24261  blssps  24312  blss  24313  blssexps  24314  blssex  24315  mopni3  24382  blcld  24393  metrest  24412  metcnp3  24428  reperflem  24707  icccmplem3  24713  xrge0tsms  24723  mulc1cncf  24798  cncfco  24800  cnheibor  24854  bndth  24857  lebnumlem3  24862  xlebnum  24864  lebnumii  24865  nmhmcn  25020  cfil3i  25169  cmetcaulem  25188  cfilres  25196  bcthlem4  25227  ivthlem2  25353  ivthlem3  25354  ivthicc  25359  cniccbdd  25362  ovolunlem1  25398  ovoliunlem2  25404  ovolshftlem2  25411  ovolicc2  25423  iunmbl2  25458  dyadmax  25499  opnmbllem  25502  subopnmbl  25505  volivth  25508  ismbf3d  25555  mbfimaopn2  25558  mbfaddlem  25561  i1fmullem  25595  mbfi1fseqlem4  25619  bddiblnc  25743  ellimc3  25780  dvlip  25898  dvlip2  25900  c1liplem1  25901  dvgt0lem1  25907  dvivthlem2  25914  dvne0  25916  lhop1lem  25918  lhop2  25920  lhop  25921  tdeglem4  25965  mdegnn0cl  25976  ply1divex  26042  dvdsq1p  26068  ig1peu  26080  elply2  26101  plypf1  26117  plydivex  26205  aalioulem3  26242  aalioulem5  26244  aaliou  26246  ulmshftlem  26298  ulmcau  26304  ulmss  26306  ulmbdd  26307  ulmcn  26308  radcnvlt1  26327  eflogeq  26511  efopn  26567  cxpeq  26667  angpieqvd  26741  xrlimcnp  26878  cxploglim  26888  ftalem2  26984  ftalem7  26989  isppw2  27025  dchrptlem1  27175  dchrptlem3  27177  dchrsum2  27179  lgsdchrval  27265  lgsdchr  27266  gausslemma2dlem1a  27276  lgsquadlem1  27291  2lgsoddprmlem2  27320  dchrisumlem3  27402  dchrisum0fno1  27422  pntlem3  27520  pntleml  27522  ostth3  27549  nosupno  27615  nosupbday  27617  noinfbday  27632  scutun12  27722  oldssmade  27789  addsproplem2  27877  addsuniflem  27908  addsbdaylem  27923  negsid  27947  negsunif  27961  precsexlem6  28114  precsexlem7  28115  precsexlem11  28119  bdayon  28173  onaddscl  28174  om2noseqlt  28193  noseqrdgfn  28200  n0sfincut  28246  bdayn0sf1o  28259  dfnns2  28261  zs12negscl  28340  zs12bday  28343  recut  28347  brcgr  28827  brbtwn2  28832  axbtwnid  28866  axcontlem7  28897  usgrnloopALT  29130  uhgrspansubgrlem  29217  nbuhgr  29270  nbupgr  29271  wwlksnextprop  29842  elwspths2on  29890  erclwwlktr  29951  clwwlknscsh  29991  erclwwlkntr  30000  hashecclwwlkn1  30006  umgrhashecclwwlk  30007  3cyclfrgrrn1  30214  frgrregorufr  30254  frgr2wwlk1  30258  ubthlem1  30799  ubthlem3  30801  htthlem  30846  omlsii  31332  spansncol  31497  nmopun  31943  nmcexi  31955  riesz1  31994  elpjrn  32119  cvcon3  32213  chcv1  32284  atcvatlem  32314  chirredi  32323  br8d  32538  xrge0tsmsd  33002  ordtrest2NEWlem  33912  lmxrge0  33942  esumfsup  34060  esumpcvgval  34068  measdivcstALTV  34215  eulerpartlemgh  34369  dstfrvunirn  34466  afsval  34662  onvf1odlem4  35093  erdszelem8  35185  erdszelem11  35188  erdsze2lem2  35191  connpconn  35222  sconnpi1  35226  cvmsss2  35261  cvmfolem  35266  cvmliftmolem2  35269  cvmliftlem15  35285  cvmlift2lem1  35289  cvmlift3lem4  35309  cvmlift3lem5  35310  satfdmlem  35355  fmla1  35374  gonarlem  35381  gonar  35382  goalrlem  35383  goalr  35384  fmla0disjsuc  35385  fmlasucdisj  35386  satffunlem1lem1  35389  satffunlem1lem2  35390  satffunlem2lem1  35391  mrsub0  35503  mrsubcn  35506  msubrn  35516  msubvrs  35547  br8  35743  br6  35744  br4  35745  cgrtriv  35990  btwntriv2  36000  btwncomim  36001  btwnswapid  36005  btwnintr  36007  btwnexch3  36008  btwnouttr2  36010  ifscgr  36032  cgrxfr  36043  btwnxfr  36044  btwnconn3  36091  segcon2  36093  brsegle  36096  seglecgr12im  36098  broutsideof3  36114  linethru  36141  elhf2  36163  opnregcld  36318  cldregopn  36319  neibastop2lem  36348  matunitlindflem1  37610  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem24  37638  poimirlem29  37643  heicant  37649  opnmbllem0  37650  ismblfin  37655  itg2addnclem  37665  itg2addnclem3  37667  itg2gt0cn  37669  ftc1anclem5  37691  ftc2nc  37696  filbcmb  37734  fdc  37739  incsequz  37742  caushft  37755  istotbnd3  37765  equivbnd  37784  cntotbnd  37790  heibor1lem  37803  heibor1  37804  bfplem2  37817  divrngidl  38022  prnc  38061  lshpdisj  38980  cvrcon3b  39270  atnle  39310  hlhgt2  39383  hl0lt1N  39384  hl2at  39399  cvrexchlem  39413  cvratlem  39415  lvolnlelpln  39579  2lplnj  39614  ispsubcl2N  39941  lautcvr  40086  dva1dim  40979  dib1dim  41159  dib1dim2  41162  diclspsn  41188  dih1dimatlem  41323  dihlatat  41331  dihatexv  41332  dihatexv2  41333  lcfrlem9  41544  lcfrlem16  41552  mapdrvallem2  41639  mapd1o  41642  aks6d1c2  42118  elre0re  42242  prjspner1  42614  dffltz  42622  rexlimdv3d  42671  elrfi  42682  isnacs3  42698  eldiophb  42745  eldiophss  42762  diophren  42801  rencldnfilem  42808  pell1234qrdich  42849  pellfundex  42874  lsmfgcl  43063  kercvrlsm  43072  lmhmfgima  43073  lpirlnr  43106  hbtlem2  43113  hbtlem4  43115  hbtlem6  43118  rngunsnply  43158  onexoegt  43233  oaabsb  43283  cantnfresb  43313  omabs2  43321  tfsconcatrev  43337  restuni3  45112  limsupubuz  45711  stoweidlem57  46055  fourierdlem48  46152  fourierdlem49  46153  sge0le  46405  fsetsniunop  47047  cfsetsnfsetfo  47058  fcoresf1  47067  euoreqb  47107  modlt0b  47361  imasetpreimafvbijlemf1  47402  imasetpreimafvbijlemfo  47403  iccpartrn  47428  iccpartiun  47432  iccpartnel  47436  paireqne  47509  reupr  47520  odz2prm2pw  47561  fmtnofac2lem  47566  prmdvdsfmtnof1lem2  47583  2pwp1prm  47587  mod42tp1mod8  47600  lighneallem3  47605  lighneallem4  47608  requad01  47619  requad2  47621  fppr2odd  47729  gbowpos  47757  gbowgt5  47760  gboge9  47762  nnsum4primesodd  47794  nnsum4primesoddALTV  47795  isubgredg  47863  grimcnv  47885  uhgrimedgi  47887  isuspgrim0  47891  isuspgrimlem  47892  gricushgr  47914  clnbgrgrimlem  47930  clnbgrgrim  47931  grimedg  47932  grtrissvtx  47940  stgrusgra  47955  isubgr3stgrlem7  47968  gpgiedgdmellem  48034  gpgusgralem  48044  gpgvtxedg0  48051  gpgvtxedg1  48052  copisnmnd  48154  lidldomn1  48216  affinecomb1  48688  eenglngeehlnmlem2  48724  rrx2vlinest  48727  itsclquadb  48762  aacllem  49787