Theorem rexlimdva 3165

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 418	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	rexlimdv 3163	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ∃wrex 3088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3089

This theorem is used by:  rexlimdvaa  3166  rexlimivv  3206  rexlimdvv  3220  rspceb2dv  3583  ssexnelpss  4068  ralxfrd2  5381  iunopeqop  5502  iunopeqopOLD  5503  elsnxp  6293  foco2  7106  elunirn  7252  f1elima  7264  mptcnfimad  7987  releldmdifi  8046  mpoexw  8081  xpord3pred  8154  sexp3  8155  tfrlem9a  8379  seqomlem2  8444  oawordexr  8547  odi  8570  oelimcl  8592  nnawordex  8629  nnaordex  8630  oaabs  8640  oaabs2  8641  omabs  8643  eldifsucnn  8656  coflton  8663  cofon1  8664  cofon2  8665  cofonr  8666  naddunif  8686  ectocld  8786  onfin  9213  dif1ennnALT  9251  isfinite2  9272  isfiniteg  9274  fofinf1o  9303  elfiun  9404  suplub2  9435  supisoex  9449  ordtypelem9  9502  ordtypelem10  9503  brwdom2  9549  brwdom3  9558  ttrcltr  9699  rankr1ai  9784  fodomfi2  10067  infpwfien  10069  dfac12r  10153  ackbij1  10243  cff1  10264  fin23lem21  10345  isf32lem2  10360  fin1a2lem11  10416  fin1a2lem13  10418  ficard  10577  gchina  10712  eltsk2g  10764  tskr1om2  10781  rankcf  10790  inatsk  10791  tskuni  10796  nqereu  10942  ltexnq  10988  1idpr  11042  suplem1pr  11065  supsrlem  11124  axpre-sup  11182  1re  11236  0re  11238  0cnALT  11473  supaddc  12210  supadd  12211  supmul1  12212  supmul  12215  suprzcl2  12991  qmulz  13004  elpq  13029  qbtwnre  13255  ioo0  13427  ico0  13448  ioc0  13449  icc0  13450  addmodlteq  14014  fsequb  14043  hashdom  14447  ccats1alpha  14691  reuccatpfxs1lem  14819  shftlem  15145  rexuzre  15444  rexico  15445  caubnd  15450  limsupbnd1  15573  limsupbnd2  15574  rlim2lt  15588  rlim3  15589  lo1bdd2  15615  lo1bddrp  15616  o1lo1  15628  climuni  15643  climshftlem  15665  o1co  15677  rlimcn1  15679  climcn1  15683  o1rlimmul  15710  lo1le  15743  rlimno1  15745  isercoll  15759  caurcvg2  15769  serf0  15772  summolem2  15806  zsum  15808  fsum2dlem  15860  geomulcvg  15969  mertenslem2  15978  ntrivcvg  15990  zprod  16030  fprod2dlem  16073  dvds1lem  16363  dvdsexp2im  16423  odd2np1lem  16436  sqoddm1div8z  16450  ltoddhalfle  16457  halfleoddlt  16458  flodddiv4  16511  dvdssqim  16650  dvdsexpim  16651  coprmdvds2  16750  divgcdcoprm0  16761  cncongr1  16763  cncongr2  16764  isprm5  16804  rpexp  16819  pythagtriplem1  16914  iserodd  16933  pc2dvds  16977  difsqpwdvds  16985  oddprmdvds  17001  prmpwdvds  17002  4sqlem11  17053  vdwapun  17072  vdwlem2  17080  vdwlem6  17084  vdwlem8  17086  vdwlem10  17088  vdwnnlem1  17093  vdwnnlem3  17095  0ram  17118  ramub1lem2  17125  ramcl  17127  cshwsiun  17197  cshwrepswhash1  17200  firest  17523  imasvscafn  17629  imasmgm2  18782  imasmnd2  18887  dfgrp3lem  19167  imasgrp2  19184  issubg4  19275  cycsubm  19336  gaorber  19441  orbsta  19446  pmtr3ncom  19608  psgnran  19648  odmulg  19689  odbezout  19691  gexdvdsi  19716  sylow1lem3  19733  odcau  19737  sylow2alem1  19750  sylow3lem6  19765  lsmelvalm  19784  efgrelexlemb  19883  efgredeu  19885  imasabl  20009  cyggeninv  20016  cygctb  20025  cyggexb  20032  dprdssv  20151  dprddisj2  20174  ablfacrplem  20200  pgpfac1lem2  20210  pgpfac1lem5  20214  ringinvnzdiv  20449  imasring  20477  dvdsrcl2  20513  dvdsrmul1  20516  lss1d  21153  lssats2  21190  lspsn  21192  lmhmima  21237  rspsn0  21441  ring2idlqusb  21519  rngqiprngfulem2  21521  lpiss  21566  dvdsrzring  21680  pzriprnglem5  21704  pzriprnglem8  21707  pzriprnglem10  21709  pzriprnglem11  21710  znunit  21782  znrrg  21784  cygznlem3  21788  frgpcyg  21792  lindfrn  22040  mplcoe5lem  22261  mpfind  22337  gsummoncoe1  22539  mpfpf1  22582  pf1mpf  22583  mat1dimelbas  22699  scmatdmat  22743  scmataddcl  22744  scmatsubcl  22745  scmatmulcl  22746  matunitlindflem1  22907  cpmatacl  22947  chpscmat  23073  tgcl  23200  clsval2  23281  innei  23356  restcld  23403  restcldr  23405  ordtrest2lem  23434  cnprest  23520  lmss  23529  lmcls  23533  lmcnp  23535  isreg2  23608  cmpcovf  23622  cncmp  23623  cmpsub  23631  1stcrest  23684  2ndcrest  23685  1stccnp  23694  restnlly  23714  cldllycmp  23727  locfincmp  23758  txcnpi  23840  pthaus  23870  txtube  23872  txcmplem1  23873  txcmplem2  23874  txlm  23880  xkohaus  23885  xkococnlem  23891  xkococn  23892  kqfvima  23962  kqreglem1  23973  isfild  24090  filuni  24117  isufil2  24140  uffix  24153  rnelfm  24185  fmfnfmlem2  24187  fmfnfmlem4  24189  fmfnfm  24190  fmco  24193  fclsopn  24246  ufilcmp  24264  cnpfcf  24273  alexsublem  24276  alexsubALT  24283  cldsubg  24343  ghmcnp  24347  qustgpopn  24352  tsmsgsum  24371  tsmsres  24376  tsmsxplem1  24385  tsmsxp  24387  isucn2  24510  ucnprima  24513  imasdsf1olem  24605  blssps  24656  blss  24657  blssexps  24658  blssex  24659  mopni3  24726  blcld  24737  metrest  24756  metcnp3  24772  reperflem  25051  icccmplem3  25057  xrge0tsms  25067  mulc1cncf  25139  cncfco  25141  cnheibor  25189  bndth  25192  lebnumlem3  25197  xlebnum  25199  lebnumii  25200  nmhmcn  25354  cfil3i  25503  cmetcaulem  25522  cfilres  25530  bcthlem4  25561  ivthlem2  25686  ivthlem3  25687  ivthicc  25692  cniccbdd  25695  ovolunlem1  25731  ovoliunlem2  25737  ovolshftlem2  25744  ovolicc2  25756  iunmbl2  25791  dyadmax  25832  opnmbllem  25835  subopnmbl  25838  volivth  25841  ismbf3d  25888  mbfimaopn2  25891  mbfaddlem  25894  i1fmullem  25928  mbfi1fseqlem4  25952  bddiblnc  26076  ellimc3  26113  dvlip  26227  dvlip2  26229  c1liplem1  26230  dvgt0lem1  26236  dvivthlem2  26243  dvne0  26245  lhop1lem  26247  lhop2  26249  lhop  26250  tdeglem4  26292  mdegnn0cl  26303  ply1divex  26369  dvdsq1p  26395  ig1peu  26407  elply2  26428  plypf1  26445  plydivex  26534  aalioulem3  26577  aalioulem5  26579  aaliou  26581  ulmshftlem  26632  ulmcau  26638  ulmss  26640  ulmbdd  26641  ulmcn  26642  radcnvlt1  26661  eflogeq  26847  efopn  26903  cxpeq  27002  angpieqvd  27076  xrlimcnp  27213  cxploglim  27222  ftalem2  27318  ftalem7  27323  isppw2  27359  dchrptlem1  27508  dchrptlem3  27510  dchrsum2  27512  lgsdchrval  27598  lgsdchr  27599  gausslemma2dlem1a  27609  lgsquadlem1  27624  2lgsoddprmlem2  27653  dchrisumlem3  27735  dchrisum0fno1  27755  pntlem3  27853  pntleml  27855  ostth3  27882  nosupno  27947  nosupbday  27949  noinfbday  27964  cutsun12  28063  oldssmade  28140  addsproplem2  28243  addsuniflem  28274  addbdaylem  28290  negsid  28314  negsunif  28328  negleft  28331  negright  28332  precsexlem6  28485  precsexlem7  28486  precsexlem11  28490  bdayons  28549  onaddscl  28550  om2noseqlt  28572  noseqrdgfn  28579  n0fincut  28628  bdayn0sf1o  28643  dfnns2  28645  bdaypw2n0bndlem  28736  bdayfinbndlem1  28740  z12negscl  28751  z12zsodd  28755  z12bdaylem  28757  bdayfinlem  28759  recut  28767  elreno2  28768  brcgr  29365  brbtwn2  29370  axbtwnid  29404  axcontlem7  29435  usgrnloopALT  29671  uhgrspansubgrlem  29758  nbuhgr  29811  nbupgr  29812  wwlksnextprop  30388  elwspths2on  30438  elwspths2onw  30439  erclwwlktr  30500  clwwlknscsh  30540  erclwwlkntr  30549  hashecclwwlkn1  30555  umgrhashecclwwlk  30556  3cyclfrgrrn1  30773  frgrregorufr  30813  frgr2wwlk1  30817  ubthlem1  31359  ubthlem3  31361  htthlem  31406  omlsii  31892  spansncol  32057  nmopun  32503  nmcexi  32515  riesz1  32554  elpjrn  32679  cvcon3  32773  chcv1  32844  atcvatlem  32874  chirredi  32883  br8d  33089  xrge0tsmsd  33521  ordtrest2NEWlem  34440  lmxrge0  34470  esumfsup  34588  esumpcvgval  34596  measdivcstALTV  34744  eulerpartlemgh  34897  dstfrvunirn  34994  afsval  35190  onvf1odlem4  35711  erdszelem8  35785  erdszelem11  35788  erdsze2lem2  35791  connpconn  35822  sconnpi1  35826  cvmsss2  35861  cvmfolem  35866  cvmliftmolem2  35869  cvmliftlem15  35885  cvmlift2lem1  35889  cvmlift3lem4  35909  cvmlift3lem5  35910  satfdmlem  35955  fmla1  35974  gonarlem  35981  gonar  35982  goalrlem  35983  goalr  35984  fmla0disjsuc  35985  fmlasucdisj  35986  satffunlem1lem1  35989  satffunlem1lem2  35990  satffunlem2lem1  35991  mrsub0  36103  mrsubcn  36106  msubrn  36116  msubvrs  36147  br8  36343  br6  36344  br4  36345  cgrtriv  36590  btwntriv2  36600  btwncomim  36601  btwnswapid  36605  btwnintr  36607  btwnexch3  36608  btwnouttr2  36610  ifscgr  36632  cgrxfr  36643  btwnxfr  36644  btwnconn3  36691  segcon2  36693  brsegle  36696  seglecgr12im  36698  broutsideof3  36714  linethru  36741  elhf2  36763  nmulprop  36778  opnregcld  36957  cldregopn  36958  neibastop2lem  36987  tr0elw  37111  tr0el  37112  poimirlem16  38393  poimirlem17  38394  poimirlem19  38396  poimirlem20  38397  poimirlem24  38401  poimirlem29  38406  heicant  38412  opnmbllem0  38413  ismblfin  38418  itg2addnclem  38428  itg2addnclem3  38430  itg2gt0cn  38432  ftc1anclem5  38454  ftc2nc  38459  filbcmb  38498  fdc  38503  incsequz  38506  caushft  38519  istotbnd3  38529  equivbnd  38548  cntotbnd  38554  heibor1lem  38567  heibor1  38568  bfplem2  38581  divrngidl  38786  prnc  38825  lshpdisj  39868  cvrcon3b  40158  atnle  40198  hlhgt2  40270  hl0lt1N  40271  hl2at  40286  cvrexchlem  40300  cvratlem  40302  lvolnlelpln  40466  2lplnj  40501  ispsubcl2N  40828  lautcvr  40973  dva1dim  41866  dib1dim  42046  dib1dim2  42049  diclspsn  42075  dih1dimatlem  42210  dihlatat  42218  dihatexv  42219  dihatexv2  42220  lcfrlem9  42431  lcfrlem16  42439  mapdrvallem2  42526  mapd1o  42529  aks6d1c2  43004  elre0re  43129  prjspner1  43480  dffltz  43488  rexlimdv3d  43536  elrfi  43547  isnacs3  43563  eldiophb  43610  eldiophss  43627  diophren  43662  rencldnfilem  43669  pell1234qrdich  43710  pellfundex  43735  lsmfgcl  43923  kercvrlsm  43932  lmhmfgima  43933  lpirlnr  43966  hbtlem2  43973  hbtlem4  43975  hbtlem6  43978  rngunsnply  44018  onexoegt  44093  oaabsb  44143  cantnfresb  44173  omabs2  44181  tfsconcatrev  44197  restuni3  45958  limsupubuz  46549  stoweidlem57  46893  fourierdlem48  46990  fourierdlem49  46991  sge0le  47243  fsetsniunop  47945  cfsetsnfsetfo  47956  fcoresf1  47965  euoreqb  48005  modlt0b  48265  nndivides2  48280  imasetpreimafvbijlemf1  48312  imasetpreimafvbijlemfo  48313  iccpartrn  48338  iccpartiun  48342  iccpartnel  48346  paireqne  48419  reupr  48430  odz2prm2pw  48474  fmtnofac2lem  48479  prmdvdsfmtnof1lem2  48496  2pwp1prm  48500  mod42tp1mod8  48513  lighneallem3  48518  lighneallem4  48521  nprmdvdsfacm1  48535  ppivalnnprm  48536  ppivalnnnprmge6  48537  requad01  48545  requad2  48547  fppr2odd  48655  gbowpos  48683  gbowgt5  48686  gboge9  48688  nnsum4primesodd  48720  nnsum4primesoddALTV  48721  isubgredg  48790  grimcnv  48812  uhgrimedgi  48814  isuspgrim0  48818  isuspgrimlem  48819  gricushgr  48841  clnbgrgrimlem  48857  clnbgrgrim  48858  grimedg  48859  grtrissvtx  48868  stgrusgra  48883  isubgr3stgrlem7  48896  gpgiedgdmellem  48970  gpgusgralem  48980  gpgvtxedg0  48987  gpgvtxedg1  48988  copisnmnd  49092  lidldomn1  49154  affinecomb1  49640  eenglngeehlnmlem2  49676  rrx2vlinest  49679  itsclquadb  49714  aacllem  50780