Theorem rexlimdva 3155

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 3153	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∃wrex 3070

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 3071

This theorem is referenced by:  rexlimdvaa  3156  rexlimivv  3201  rexlimdvv  3212  rspceb2dv  3626  ssexnelpss  4116  ralxfrd2  5412  iunopeqop  5526  elsnxp  6311  foco2  7129  elunirn  7271  f1elima  7283  mptcnfimad  8011  releldmdifi  8070  mpoexw  8103  xpord3pred  8177  sexp3  8178  tfrlem9a  8426  seqomlem2  8491  oawordexr  8594  odi  8617  oelimcl  8638  nnawordex  8675  nnaordex  8676  oaabs  8686  oaabs2  8687  omabs  8689  eldifsucnn  8702  coflton  8709  cofon1  8710  cofon2  8711  cofonr  8712  naddunif  8731  ectocld  8824  onfin  9267  dif1ennnALT  9311  isfinite2  9334  isfiniteg  9337  fofinf1o  9372  elfiun  9470  suplub2  9501  supisoex  9514  ordtypelem9  9566  ordtypelem10  9567  brwdom2  9613  brwdom3  9622  ttrcltr  9756  rankr1ai  9838  fodomfi2  10100  infpwfien  10102  dfac12r  10187  ackbij1  10277  cff1  10298  fin23lem21  10379  isf32lem2  10394  fin1a2lem11  10450  fin1a2lem13  10452  ficard  10605  gchina  10739  eltsk2g  10791  tskr1om2  10808  rankcf  10817  inatsk  10818  tskuni  10823  nqereu  10969  ltexnq  11015  1idpr  11069  suplem1pr  11092  supsrlem  11151  axpre-sup  11209  1re  11261  0re  11263  0cnALT  11496  supaddc  12235  supadd  12236  supmul1  12237  supmul  12240  suprzcl2  12980  qmulz  12993  elpq  13017  qbtwnre  13241  ioo0  13412  ico0  13433  ioc0  13434  icc0  13435  addmodlteq  13987  fsequb  14016  hashdom  14418  ccats1alpha  14657  reuccatpfxs1lem  14784  shftlem  15107  rexuzre  15391  rexico  15392  caubnd  15397  limsupbnd1  15518  limsupbnd2  15519  rlim2lt  15533  rlim3  15534  lo1bdd2  15560  lo1bddrp  15561  o1lo1  15573  climuni  15588  climshftlem  15610  o1co  15622  rlimcn1  15624  climcn1  15628  o1rlimmul  15655  lo1le  15688  rlimno1  15690  isercoll  15704  caurcvg2  15714  serf0  15717  summolem2  15752  zsum  15754  fsum2dlem  15806  geomulcvg  15912  mertenslem2  15921  ntrivcvg  15933  zprod  15973  fprod2dlem  16016  dvds1lem  16305  dvdsexp2im  16364  odd2np1lem  16377  sqoddm1div8z  16391  ltoddhalfle  16398  halfleoddlt  16399  flodddiv4  16452  dvdssqim  16591  dvdsexpim  16592  coprmdvds2  16691  divgcdcoprm0  16702  cncongr1  16704  cncongr2  16705  isprm5  16744  rpexp  16759  pythagtriplem1  16854  iserodd  16873  pc2dvds  16917  difsqpwdvds  16925  oddprmdvds  16941  prmpwdvds  16942  4sqlem11  16993  vdwapun  17012  vdwlem2  17020  vdwlem6  17024  vdwlem8  17026  vdwlem10  17028  vdwnnlem1  17033  vdwnnlem3  17035  0ram  17058  ramub1lem2  17065  ramcl  17067  cshwsiun  17137  cshwrepswhash1  17140  firest  17477  imasvscafn  17582  imasmnd2  18787  dfgrp3lem  19056  imasgrp2  19073  issubg4  19163  cycsubm  19220  gaorber  19326  orbsta  19331  pmtr3ncom  19493  psgnran  19533  odmulg  19574  odbezout  19576  gexdvdsi  19601  sylow1lem3  19618  odcau  19622  sylow2alem1  19635  sylow3lem6  19650  lsmelvalm  19669  efgrelexlemb  19768  efgredeu  19770  imasabl  19894  cyggeninv  19901  cygctb  19910  cyggexb  19917  dprdssv  20036  dprddisj2  20059  ablfacrplem  20085  pgpfac1lem2  20095  pgpfac1lem5  20099  ringinvnzdiv  20298  imasring  20327  dvdsrcl2  20366  dvdsrmul1  20369  lss1d  20961  lssats2  20998  lspsn  21000  lmhmima  21046  ring2idlqusb  21320  rngqiprngfulem2  21322  lpiss  21339  dvdsrzring  21472  pzriprnglem5  21496  pzriprnglem8  21499  pzriprnglem10  21501  pzriprnglem11  21502  znunit  21582  znrrg  21584  cygznlem3  21588  frgpcyg  21592  lindfrn  21841  mplcoe5lem  22057  mpfind  22131  gsummoncoe1  22312  mpfpf1  22355  pf1mpf  22356  mat1dimelbas  22477  scmatdmat  22521  scmataddcl  22522  scmatsubcl  22523  scmatmulcl  22524  cpmatacl  22722  chpscmat  22848  tgcl  22976  clsval2  23058  innei  23133  restcld  23180  restcldr  23182  ordtrest2lem  23211  cnprest  23297  lmss  23306  lmcls  23310  lmcnp  23312  isreg2  23385  cmpcovf  23399  cncmp  23400  cmpsub  23408  1stcrest  23461  2ndcrest  23462  1stccnp  23470  restnlly  23490  cldllycmp  23503  locfincmp  23534  txcnpi  23616  pthaus  23646  txtube  23648  txcmplem1  23649  txcmplem2  23650  txlm  23656  xkohaus  23661  xkococnlem  23667  xkococn  23668  kqfvima  23738  kqreglem1  23749  isfild  23866  filuni  23893  isufil2  23916  uffix  23929  rnelfm  23961  fmfnfmlem2  23963  fmfnfmlem4  23965  fmfnfm  23966  fmco  23969  fclsopn  24022  ufilcmp  24040  cnpfcf  24049  alexsublem  24052  alexsubALT  24059  cldsubg  24119  ghmcnp  24123  qustgpopn  24128  tsmsgsum  24147  tsmsres  24152  tsmsxplem1  24161  tsmsxp  24163  isucn2  24288  ucnprima  24291  imasdsf1olem  24383  blssps  24434  blss  24435  blssexps  24436  blssex  24437  mopni3  24507  blcld  24518  metrest  24537  metcnp3  24553  reperflem  24840  icccmplem3  24846  xrge0tsms  24856  mulc1cncf  24931  cncfco  24933  cnheibor  24987  bndth  24990  lebnumlem3  24995  xlebnum  24997  lebnumii  24998  nmhmcn  25153  cfil3i  25303  cmetcaulem  25322  cfilres  25330  bcthlem4  25361  ivthlem2  25487  ivthlem3  25488  ivthicc  25493  cniccbdd  25496  ovolunlem1  25532  ovoliunlem2  25538  ovolshftlem2  25545  ovolicc2  25557  iunmbl2  25592  dyadmax  25633  opnmbllem  25636  subopnmbl  25639  volivth  25642  ismbf3d  25689  mbfimaopn2  25692  mbfaddlem  25695  i1fmullem  25729  mbfi1fseqlem4  25753  bddiblnc  25877  ellimc3  25914  dvlip  26032  dvlip2  26034  c1liplem1  26035  dvgt0lem1  26041  dvivthlem2  26048  dvne0  26050  lhop1lem  26052  lhop2  26054  lhop  26055  tdeglem4  26099  mdegnn0cl  26110  ply1divex  26176  dvdsq1p  26202  ig1peu  26214  elply2  26235  plypf1  26251  plydivex  26339  aalioulem3  26376  aalioulem5  26378  aaliou  26380  ulmshftlem  26432  ulmcau  26438  ulmss  26440  ulmbdd  26441  ulmcn  26442  radcnvlt1  26461  eflogeq  26644  efopn  26700  cxpeq  26800  angpieqvd  26874  xrlimcnp  27011  cxploglim  27021  ftalem2  27117  ftalem7  27122  isppw2  27158  dchrptlem1  27308  dchrptlem3  27310  dchrsum2  27312  lgsdchrval  27398  lgsdchr  27399  gausslemma2dlem1a  27409  lgsquadlem1  27424  2lgsoddprmlem2  27453  dchrisumlem3  27535  dchrisum0fno1  27555  pntlem3  27653  pntleml  27655  ostth3  27682  nosupno  27748  nosupbday  27750  noinfbday  27765  scutun12  27855  oldssmade  27916  addsproplem2  28003  addsuniflem  28034  addsbdaylem  28049  negsid  28073  negsunif  28087  precsexlem6  28236  precsexlem7  28237  precsexlem11  28241  onaddscl  28286  om2noseqlt  28305  noseqrdgfn  28312  dfnns2  28362  zs12bday  28424  recut  28428  brcgr  28915  brbtwn2  28920  axbtwnid  28954  axcontlem7  28985  usgrnloopALT  29220  uhgrspansubgrlem  29307  nbuhgr  29360  nbupgr  29361  wwlksnextprop  29932  elwspths2on  29980  erclwwlktr  30041  clwwlknscsh  30081  erclwwlkntr  30090  hashecclwwlkn1  30096  umgrhashecclwwlk  30097  3cyclfrgrrn1  30304  frgrregorufr  30344  frgr2wwlk1  30348  ubthlem1  30889  ubthlem3  30891  htthlem  30936  omlsii  31422  spansncol  31587  nmopun  32033  nmcexi  32045  riesz1  32084  elpjrn  32209  cvcon3  32303  chcv1  32374  atcvatlem  32404  chirredi  32413  br8d  32622  xrge0tsmsd  33065  ordtrest2NEWlem  33921  lmxrge0  33951  esumfsup  34071  esumpcvgval  34079  measdivcstALTV  34226  eulerpartlemgh  34380  dstfrvunirn  34477  afsval  34686  erdszelem8  35203  erdszelem11  35206  erdsze2lem2  35209  connpconn  35240  sconnpi1  35244  cvmsss2  35279  cvmfolem  35284  cvmliftmolem2  35287  cvmliftlem15  35303  cvmlift2lem1  35307  cvmlift3lem4  35327  cvmlift3lem5  35328  satfdmlem  35373  fmla1  35392  gonarlem  35399  gonar  35400  goalrlem  35401  goalr  35402  fmla0disjsuc  35403  fmlasucdisj  35404  satffunlem1lem1  35407  satffunlem1lem2  35408  satffunlem2lem1  35409  mrsub0  35521  mrsubcn  35524  msubrn  35534  msubvrs  35565  br8  35756  br6  35757  br4  35758  cgrtriv  36003  btwntriv2  36013  btwncomim  36014  btwnswapid  36018  btwnintr  36020  btwnexch3  36021  btwnouttr2  36023  ifscgr  36045  cgrxfr  36056  btwnxfr  36057  btwnconn3  36104  segcon2  36106  brsegle  36109  seglecgr12im  36111  broutsideof3  36127  linethru  36154  elhf2  36176  opnregcld  36331  cldregopn  36332  neibastop2lem  36361  matunitlindflem1  37623  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem24  37651  poimirlem29  37656  heicant  37662  opnmbllem0  37663  ismblfin  37668  itg2addnclem  37678  itg2addnclem3  37680  itg2gt0cn  37682  ftc1anclem5  37704  ftc2nc  37709  filbcmb  37747  fdc  37752  incsequz  37755  caushft  37768  istotbnd3  37778  equivbnd  37797  cntotbnd  37803  heibor1lem  37816  heibor1  37817  bfplem2  37830  divrngidl  38035  prnc  38074  lshpdisj  38988  cvrcon3b  39278  atnle  39318  hlhgt2  39391  hl0lt1N  39392  hl2at  39407  cvrexchlem  39421  cvratlem  39423  lvolnlelpln  39587  2lplnj  39622  ispsubcl2N  39949  lautcvr  40094  dva1dim  40987  dib1dim  41167  dib1dim2  41170  diclspsn  41196  dih1dimatlem  41331  dihlatat  41339  dihatexv  41340  dihatexv2  41341  lcfrlem9  41552  lcfrlem16  41560  mapdrvallem2  41647  mapd1o  41650  aks6d1c2  42131  elre0re  42295  prjspner1  42636  dffltz  42644  rexlimdv3d  42694  elrfi  42705  isnacs3  42721  eldiophb  42768  eldiophss  42785  diophren  42824  rencldnfilem  42831  pell1234qrdich  42872  pellfundex  42897  lsmfgcl  43086  kercvrlsm  43095  lmhmfgima  43096  lpirlnr  43129  hbtlem2  43136  hbtlem4  43138  hbtlem6  43141  rngunsnply  43181  onexoegt  43256  oaabsb  43307  cantnfresb  43337  omabs2  43345  tfsconcatrev  43361  restuni3  45123  limsupubuz  45728  stoweidlem57  46072  fourierdlem48  46169  fourierdlem49  46170  sge0le  46422  fsetsniunop  47061  cfsetsnfsetfo  47072  fcoresf1  47081  euoreqb  47121  imasetpreimafvbijlemf1  47391  imasetpreimafvbijlemfo  47392  iccpartrn  47417  iccpartiun  47421  iccpartnel  47425  paireqne  47498  reupr  47509  odz2prm2pw  47550  fmtnofac2lem  47555  prmdvdsfmtnof1lem2  47572  2pwp1prm  47576  mod42tp1mod8  47589  lighneallem3  47594  lighneallem4  47597  requad01  47608  requad2  47610  fppr2odd  47718  gbowpos  47746  gbowgt5  47749  gboge9  47751  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  isubgredg  47852  isuspgrim0  47872  isuspgrimlem  47874  grimcnv  47879  gricushgr  47886  clnbgrgrimlem  47901  clnbgrgrim  47902  grimedg  47903  grtrissvtx  47911  stgrusgra  47926  isubgr3stgrlem7  47939  gpgedgel  48007  gpgusgralem  48011  gpgvtxedg0  48021  gpgvtxedg1  48022  copisnmnd  48085  lidldomn1  48147  affinecomb1  48623  eenglngeehlnmlem2  48659  rrx2vlinest  48662  itsclquadb  48697  aacllem  49320