Theorem rexlimdva 3167

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

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

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 1945

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

This theorem is used by:  rexlimdvaa  3168  rexlimivv  3208  rexlimdvv  3222  rspceb2dv  3584  ssexnelpss  4047  ralxfrd2  5379  iunopeqop  5499  iunopeqopOLD  5500  elsnxp  6315  foco2  7136  elunirn  7281  f1elima  7293  mptcnfimad  8025  releldmdifi  8084  mpoexw  8119  xpord3pred  8199  sexp3  8200  tfrlem9a  8425  seqomlem2  8492  oawordexr  8595  odi  8618  oelimcl  8640  nnawordex  8677  nnaordex  8678  oaabs  8688  oaabs2  8689  omabs  8691  eldifsucnn  8704  coflton  8711  cofon1  8712  cofon2  8713  cofonr  8714  naddunif  8734  ectocld  8834  onfin  9261  dif1ennnALT  9299  isfinite2  9321  isfiniteg  9323  fofinf1o  9352  elfiun  9452  suplub2  9483  supisoex  9497  ordtypelem9  9550  ordtypelem10  9551  brwdom2  9597  brwdom3  9606  ttrcltr  9747  rankr1ai  9836  elhf2  9940  fodomfi2  10169  infpwfien  10171  dfac12r  10255  ackbij1  10345  cff1  10366  fin23lem21  10447  isf32lem2  10462  fin1a2lem11  10518  fin1a2lem13  10520  ficard  10679  gchina  10814  eltsk2g  10866  tskhf  10883  rankcf  10892  inatsk  10893  tskuni  10898  nqereu  11044  ltexnq  11090  1idpr  11144  suplem1pr  11167  supsrlem  11226  axpre-sup  11284  1re  11338  0re  11340  0cnALT  11575  supaddc  12314  supadd  12315  supmul1  12316  supmul  12319  suprzcl2  13095  qmulz  13108  elpq  13133  qbtwnre  13359  ioo0  13531  ico0  13552  ioc0  13553  icc0  13554  addmodlteq  14119  fsequb  14148  hashdom  14553  ccats1alpha  14798  reuccatpfxs1lem  14926  shftlem  15253  rexuzre  15552  rexico  15553  caubnd  15558  limsupbnd1  15681  limsupbnd2  15682  rlim2lt  15696  rlim3  15697  lo1bdd2  15723  lo1bddrp  15724  o1lo1  15736  climuni  15751  climshftlem  15773  o1co  15785  rlimcn1  15787  climcn1  15791  o1rlimmul  15818  lo1le  15851  rlimno1  15853  isercoll  15867  caurcvg2  15877  serf0  15880  summolem2  15914  zsum  15916  fsum2dlem  15968  geomulcvg  16077  mertenslem2  16086  ntrivcvg  16098  zprod  16136  fprod2dlem  16179  dvds1lem  16469  dvdsexp2im  16529  odd2np1lem  16542  sqoddm1div8z  16556  ltoddhalfle  16563  halfleoddlt  16564  flodddiv4  16617  dvdssqim  16759  dvdsexpim  16760  coprmdvds2  16861  divgcdcoprm0  16872  cncongr1  16874  cncongr2  16875  isprm5  16915  rpexp  16930  pythagtriplem1  17026  iserodd  17045  pc2dvds  17089  difsqpwdvds  17097  oddprmdvds  17113  prmpwdvds  17114  4sqlem11  17165  vdwapun  17184  vdwlem2  17192  vdwlem6  17196  vdwlem8  17198  vdwlem10  17200  vdwnnlem1  17205  vdwnnlem3  17207  0ram  17230  ramub1lem2  17237  ramcl  17239  cshwsiun  17309  cshwrepswhash1  17312  firest  17635  imasvscafn  17741  imasmgm2  18895  imasmnd2  19000  dfgrp3lem  19280  imasgrp2  19297  issubg4  19388  cycsubm  19449  gaorber  19555  orbsta  19560  pmtr3ncom  19722  psgnran  19762  odmulg  19803  odbezout  19805  gexdvdsi  19830  sylow1lem3  19847  odcau  19851  sylow2alem1  19864  sylow3lem6  19879  lsmelvalm  19898  efgrelexlemb  19997  efgredeu  19999  imasabl  20123  cyggeninv  20130  cygctb  20139  cyggexb  20146  dprdssv  20265  dprddisj2  20288  ablfacrplem  20314  pgpfac1lem2  20324  pgpfac1lem5  20328  ringinvnzdiv  20565  imasring  20593  dvdsrcl2  20629  dvdsrmul1  20632  lss1d  21271  lssats2  21308  lspsn  21310  lmhmima  21355  rspsn0  21559  ring2idlqusb  21639  rngqiprngfulem2  21641  lpiss  21686  dvdsrzring  21800  pzriprnglem5  21824  pzriprnglem8  21827  pzriprnglem10  21829  pzriprnglem11  21830  znunit  21902  znrrg  21904  cygznlem3  21908  frgpcyg  21912  lindfrn  22160  mplcoe5lem  22381  mpfind  22457  gsummoncoe1  22659  mpfpf1  22702  pf1mpf  22703  mat1dimelbas  22819  scmatdmat  22863  scmataddcl  22864  scmatsubcl  22865  scmatmulcl  22866  matunitlindflem1  23027  cpmatacl  23067  chpscmat  23193  tgcl  23320  clsval2  23401  innei  23476  restcld  23523  restcldr  23525  ordtrest2lem  23554  cnprest  23640  lmss  23649  lmcls  23653  lmcnp  23655  isreg2  23728  cmpcovf  23742  cncmp  23743  cmpsub  23751  1stcrest  23804  2ndcrest  23805  1stccnp  23814  restnlly  23834  cldllycmp  23847  locfincmp  23878  txcnpi  23960  pthaus  23990  txtube  23992  txcmplem1  23993  txcmplem2  23994  txlm  24000  xkohaus  24005  xkococnlem  24011  xkococn  24012  kqfvima  24082  kqreglem1  24093  isfild  24210  filuni  24237  isufil2  24260  uffix  24273  rnelfm  24305  fmfnfmlem2  24307  fmfnfmlem4  24309  fmfnfm  24310  fmco  24313  fclsopn  24366  ufilcmp  24384  cnpfcf  24393  alexsublem  24396  alexsubALT  24403  cldsubg  24463  ghmcnp  24467  qustgpopn  24472  tsmsgsum  24491  tsmsres  24496  tsmsxplem1  24505  tsmsxp  24507  isucn2  24630  ucnprima  24633  imasdsf1olem  24725  blssps  24776  blss  24777  blssexps  24778  blssex  24779  mopni3  24846  blcld  24857  metrest  24876  metcnp3  24892  reperflem  25171  icccmplem3  25177  xrge0tsms  25187  mulc1cncf  25259  cncfco  25261  cnheibor  25309  bndth  25312  lebnumlem3  25317  xlebnum  25319  lebnumii  25320  nmhmcn  25474  cfil3i  25623  cmetcaulem  25642  cfilres  25650  bcthlem4  25681  ivthlem2  25806  ivthlem3  25807  ivthicc  25812  cniccbdd  25815  ovolunlem1  25851  ovoliunlem2  25857  ovolshftlem2  25864  ovolicc2  25876  iunmbl2  25911  dyadmax  25952  opnmbllem  25955  subopnmbl  25958  volivth  25961  ismbf3d  26008  mbfimaopn2  26011  mbfaddlem  26014  i1fmullem  26048  mbfi1fseqlem4  26072  bddiblnc  26195  ellimc3  26232  dvlip  26346  dvlip2  26348  c1liplem1  26349  dvgt0lem1  26355  dvivthlem2  26362  dvne0  26364  lhop1lem  26366  lhop2  26368  lhop  26369  tdeglem4  26411  mdegnn0cl  26422  ply1divex  26488  dvdsq1p  26514  ig1peu  26526  elply2  26547  plypf1  26564  plydivex  26651  aalioulem3  26694  aalioulem5  26696  aaliou  26698  ulmshftlem  26749  ulmcau  26755  ulmss  26757  ulmbdd  26758  ulmcn  26759  radcnvlt1  26778  eflogeq  26963  efopn  27019  cxpeq  27118  angpieqvd  27192  xrlimcnp  27329  cxploglim  27338  ftalem2  27434  ftalem7  27439  isppw2  27475  dchrptlem1  27624  dchrptlem3  27626  dchrsum2  27628  lgsdchrval  27714  lgsdchr  27715  gausslemma2dlem1a  27725  lgsquadlem1  27740  2lgsoddprmlem2  27769  dchrisumlem3  27851  dchrisum0fno1  27871  pntlem3  27969  pntleml  27971  ostth3  27998  fltoprm  28028  nosupno  28093  nosupbday  28095  noinfbday  28110  cutsun12  28209  oldssmade  28286  addsproplem2  28389  addsuniflem  28420  addbdaylem  28436  negsid  28460  negsunif  28474  negleft  28477  negright  28478  precsexlem6  28631  precsexlem7  28632  precsexlem11  28636  bdayons  28695  onaddscl  28696  om2noseqlt  28718  noseqrdgfn  28725  n0fincut  28774  bdayn0sf1o  28789  dfnns2  28791  bdaypw2n0bndlem  28882  bdayfinbndlem1  28886  z12negscl  28897  z12zsodd  28901  z12bdaylem  28903  bdayfinlem  28905  recut  28913  elreno2  28914  brcgr  29511  brbtwn2  29516  axbtwnid  29550  axcontlem7  29581  usgrnloopALT  29817  uhgrspansubgrlem  29904  nbuhgr  29957  nbupgr  29958  wwlksnextprop  30534  elwspths2on  30584  elwspths2onw  30585  erclwwlktr  30646  clwwlknscsh  30686  erclwwlkntr  30695  hashecclwwlkn1  30701  umgrhashecclwwlk  30702  3cyclfrgrrn1  30919  frgrregorufr  30959  frgr2wwlk1  30963  ubthlem1  31505  ubthlem3  31507  htthlem  31552  omlsii  32038  spansncol  32203  nmopun  32649  nmcexi  32661  riesz1  32700  elpjrn  32825  cvcon3  32919  chcv1  32990  atcvatlem  33020  chirredi  33029  br8d  33277  xrge0tsmsd  33710  ordtrest2NEWlem  34637  lmxrge0  34667  esumfsup  34785  esumpcvgval  34793  measdivcstALTV  34941  eulerpartlemgh  35093  dstfrvunirn  35190  afsval  35386  dfk12  36025  dfk22  36026  dfk32  36027  onvf1odlem4  36047  onprcf1acwevdlem1  36058  erdszelem8  36143  erdszelem11  36146  erdsze2lem2  36149  connpconn  36180  sconnpi1  36184  cvmsss2  36219  cvmfolem  36224  cvmliftmolem2  36227  cvmliftlem15  36243  cvmlift2lem1  36247  cvmlift3lem4  36267  cvmlift3lem5  36268  satfdmlem  36313  fmla1  36332  gonarlem  36339  gonar  36340  goalrlem  36341  goalr  36342  fmla0disjsuc  36343  fmlasucdisj  36344  satffunlem1lem1  36347  satffunlem1lem2  36348  satffunlem2lem1  36349  mrsub0  36461  mrsubcn  36464  msubrn  36474  msubvrs  36505  mirimanofffr  36642  br8  36712  br6  36713  br4  36714  cgrtriv  36958  btwntriv2  36968  btwncomim  36969  btwnswapid  36973  btwnintr  36975  btwnexch3  36976  btwnouttr2  36978  ifscgr  37000  cgrxfr  37011  btwnxfr  37012  btwnconn3  37059  segcon2  37061  brsegle  37064  seglecgr12im  37066  broutsideof3  37082  linethru  37109  nmulprop  37130  opnregcld  37309  cldregopn  37310  neibastop2lem  37339  tr0elw  37463  tr0el  37464  poimirlem16  38759  poimirlem17  38760  poimirlem19  38762  poimirlem20  38763  poimirlem24  38767  poimirlem29  38772  heicant  38778  opnmbllem0  38779  ismblfin  38784  itg2addnclem  38794  itg2addnclem3  38796  itg2gt0cn  38798  ftc1anclem5  38820  ftc2nc  38825  filbcmb  38877  fdc  38882  incsequz  38885  caushft  38898  istotbnd3  38908  equivbnd  38927  cntotbnd  38933  heibor1lem  38946  heibor1  38947  bfplem2  38960  divrngidl  39165  prnc  39204  lshpdisj  40247  cvrcon3b  40537  atnle  40577  hlhgt2  40649  hl0lt1N  40650  hl2at  40665  cvrexchlem  40679  cvratlem  40681  lvolnlelpln  40845  2lplnj  40880  ispsubcl2N  41207  lautcvr  41352  dva1dim  42245  dib1dim  42425  dib1dim2  42428  diclspsn  42454  dih1dimatlem  42589  dihlatat  42597  dihatexv  42598  dihatexv2  42599  lcfrlem9  42810  lcfrlem16  42818  mapdrvallem2  42905  mapd1o  42908  aks6d1c2  43383  elre0re  43509  dffltz  43874  rexlimdv3d  43897  elrfi  43909  isnacs3  43925  eldiophb  43972  eldiophss  43989  diophren  44024  rencldnfilem  44031  pell1234qrdich  44072  pellfundex  44097  lsmfgcl  44280  kercvrlsm  44289  lmhmfgima  44290  lpirlnr  44322  hbtlem2  44329  hbtlem4  44331  hbtlem6  44334  rngunsnply  44374  onexoegt  44449  oaabsb  44499  cantnfresb  44529  omabs2  44537  tfsconcatrev  44553  restuni3  46348  limsupubuz  46938  stoweidlem57  47282  fourierdlem48  47379  fourierdlem49  47380  sge0le  47632  fsetsniunop  48334  cfsetsnfsetfo  48345  fcoresf1  48354  euoreqb  48395  modlt0b  48654  nndivides2  48669  imasetpreimafvbijlemf1  48701  imasetpreimafvbijlemfo  48702  iccpartrn  48727  iccpartiun  48731  iccpartnel  48735  paireqne  48808  reupr  48819  odz2prm2pw  48863  fmtnofac2lem  48868  prmdvdsfmtnof1lem2  48885  2pwp1prm  48889  mod42tp1mod8  48902  lighneallem3  48907  lighneallem4  48910  nprmdvdsfacm1  48924  ppivalnnprm  48925  ppivalnnnprmge6  48926  requad01  48934  requad2  48936  fppr2odd  49044  gbowpos  49072  gbowgt5  49075  gboge9  49077  nnsum4primesodd  49109  nnsum4primesoddALTV  49110  isubgredg  49179  grimcnv  49201  uhgrimedgi  49203  isuspgrim0  49207  isuspgrimlem  49208  gricushgr  49230  clnbgrgrimlem  49246  clnbgrgrim  49247  grimedg  49248  grtrissvtx  49257  stgrusgra  49272  isubgr3stgrlem7  49285  gpgiedgdmellem  49359  gpgusgralem  49369  gpgvtxedg0  49376  gpgvtxedg1  49377  copisnmnd  49481  lidldomn1  49543  affinecomb1  50029  eenglngeehlnmlem2  50066  itsclquadb  50103  aacllem  51251