Theorem rexlimdva 3156

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  ∃wrex 3071

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 3072

This theorem is referenced by:  rexlimdvaa  3157  rexlimivv  3200  rexlimdvv  3211  ssexnelpss  4113  ralxfrd2  5410  iunopeqop  5521  elsnxp  6288  foco2  7106  elunirn  7247  f1elima  7259  releldmdifi  8028  mpoexw  8062  xpord3pred  8135  sexp3  8136  tfrlem9a  8383  seqomlem2  8448  oawordexr  8553  odi  8576  oelimcl  8597  nnawordex  8634  nnaordex  8635  oaabs  8644  oaabs2  8645  omabs  8647  eldifsucnn  8660  coflton  8667  cofon1  8668  cofon2  8669  cofonr  8670  naddunif  8689  ectocld  8775  onfin  9227  dif1ennnALT  9274  isfinite2  9298  isfiniteg  9301  fofinf1o  9324  elfiun  9422  suplub2  9453  supisoex  9466  ordtypelem9  9518  ordtypelem10  9519  brwdom2  9565  brwdom3  9574  ttrcltr  9708  rankr1ai  9790  fodomfi2  10052  infpwfien  10054  dfac12r  10138  ackbij1  10230  cff1  10250  fin23lem21  10331  isf32lem2  10346  fin1a2lem11  10402  fin1a2lem13  10404  ficard  10557  gchina  10691  eltsk2g  10743  tskr1om2  10760  rankcf  10769  inatsk  10770  tskuni  10775  nqereu  10921  ltexnq  10967  1idpr  11021  suplem1pr  11044  supsrlem  11103  axpre-sup  11161  1re  11211  0re  11213  0cnALT  11445  negfi  12160  supaddc  12178  supadd  12179  supmul1  12180  supmul  12183  suprzcl2  12919  qmulz  12932  elpq  12956  qbtwnre  13175  ioo0  13346  ico0  13367  ioc0  13368  icc0  13369  addmodlteq  13908  fsequb  13937  hashdom  14336  ccats1alpha  14566  reuccatpfxs1lem  14693  shftlem  15012  rexuzre  15296  rexico  15297  caubnd  15302  limsupbnd1  15423  limsupbnd2  15424  rlim2lt  15438  rlim3  15439  lo1bdd2  15465  lo1bddrp  15466  o1lo1  15478  climuni  15493  climshftlem  15515  o1co  15527  rlimcn1  15529  climcn1  15533  o1rlimmul  15560  lo1le  15595  rlimno1  15597  isercoll  15611  caurcvg2  15621  serf0  15624  summolem2  15659  zsum  15661  fsum2dlem  15713  geomulcvg  15819  mertenslem2  15828  ntrivcvg  15840  zprod  15878  fprod2dlem  15921  dvds1lem  16208  dvdsexp2im  16267  odd2np1lem  16280  sqoddm1div8z  16294  ltoddhalfle  16301  halfleoddlt  16302  flodddiv4  16353  dvdssqim  16493  coprmdvds2  16588  divgcdcoprm0  16599  cncongr1  16601  cncongr2  16602  isprm5  16641  rpexp  16656  pythagtriplem1  16746  iserodd  16765  pc2dvds  16809  difsqpwdvds  16817  oddprmdvds  16833  prmpwdvds  16834  4sqlem11  16885  vdwapun  16904  vdwlem2  16912  vdwlem6  16916  vdwlem8  16918  vdwlem10  16920  vdwnnlem1  16925  vdwnnlem3  16927  0ram  16950  ramub1lem2  16957  ramcl  16959  cshwsiun  17030  cshwrepswhash1  17033  firest  17375  imasvscafn  17480  imasmnd2  18659  dfgrp3lem  18918  imasgrp2  18935  issubg4  19020  cycsubm  19074  gaorber  19167  orbsta  19172  pmtr3ncom  19338  psgnran  19378  odmulg  19419  odbezout  19421  gexdvdsi  19446  sylow1lem3  19463  odcau  19467  sylow2alem1  19480  sylow3lem6  19495  lsmelvalm  19514  efgrelexlemb  19613  efgredeu  19615  imasabl  19739  cyggeninv  19746  cygctb  19755  cyggexb  19762  dprdssv  19881  dprddisj2  19904  ablfacrplem  19930  pgpfac1lem2  19940  pgpfac1lem5  19944  ringinvnzdiv  20107  imasring  20137  dvdsrcl2  20173  dvdsrmul1  20176  lss1d  20567  lssats2  20604  lspsn  20606  lmhmima  20651  lpiss  20881  dvdsrzring  21023  znunit  21111  znrrg  21113  cygznlem3  21117  frgpcyg  21121  lindfrn  21368  mplcoe5lem  21586  mpfind  21662  gsummoncoe1  21820  mpfpf1  21862  pf1mpf  21863  mat1dimelbas  21965  scmatdmat  22009  scmataddcl  22010  scmatsubcl  22011  scmatmulcl  22012  cpmatacl  22210  chpscmat  22336  tgcl  22464  clsval2  22546  innei  22621  restcld  22668  restcldr  22670  ordtrest2lem  22699  cnprest  22785  lmss  22794  lmcls  22798  lmcnp  22800  isreg2  22873  cmpcovf  22887  cncmp  22888  cmpsub  22896  1stcrest  22949  2ndcrest  22950  1stccnp  22958  restnlly  22978  cldllycmp  22991  locfincmp  23022  txcnpi  23104  pthaus  23134  txtube  23136  txcmplem1  23137  txcmplem2  23138  txlm  23144  xkohaus  23149  xkococnlem  23155  xkococn  23156  kqfvima  23226  kqreglem1  23237  isfild  23354  filuni  23381  isufil2  23404  uffix  23417  rnelfm  23449  fmfnfmlem2  23451  fmfnfmlem4  23453  fmfnfm  23454  fmco  23457  fclsopn  23510  ufilcmp  23528  cnpfcf  23537  alexsublem  23540  alexsubALT  23547  cldsubg  23607  ghmcnp  23611  qustgpopn  23616  tsmsgsum  23635  tsmsres  23640  tsmsxplem1  23649  tsmsxp  23651  isucn2  23776  ucnprima  23779  imasdsf1olem  23871  blssps  23922  blss  23923  blssexps  23924  blssex  23925  mopni3  23995  blcld  24006  metrest  24025  metcnp3  24041  reperflem  24326  icccmplem3  24332  xrge0tsms  24342  mulc1cncf  24413  cncfco  24415  cnheibor  24463  bndth  24466  lebnumlem3  24471  xlebnum  24473  lebnumii  24474  nmhmcn  24628  cfil3i  24778  cmetcaulem  24797  cfilres  24805  bcthlem4  24836  ivthlem2  24961  ivthlem3  24962  ivthicc  24967  cniccbdd  24970  ovolunlem1  25006  ovoliunlem2  25012  ovolshftlem2  25019  ovolicc2  25031  iunmbl2  25066  dyadmax  25107  opnmbllem  25110  subopnmbl  25113  volivth  25116  ismbf3d  25163  mbfimaopn2  25166  mbfaddlem  25169  i1fmullem  25203  mbfi1fseqlem4  25228  bddiblnc  25351  ellimc3  25388  dvlip  25502  dvlip2  25504  c1liplem1  25505  dvgt0lem1  25511  dvivthlem2  25518  dvne0  25520  lhop1lem  25522  lhop2  25524  lhop  25525  tdeglem4  25569  tdeglem4OLD  25570  mdegnn0cl  25581  ply1divex  25646  dvdsq1p  25670  ig1peu  25681  elply2  25702  plypf1  25718  plydivex  25802  aalioulem3  25839  aalioulem5  25841  aaliou  25843  ulmshftlem  25893  ulmcau  25899  ulmss  25901  ulmbdd  25902  ulmcn  25903  radcnvlt1  25922  eflogeq  26102  efopn  26158  cxpeq  26255  angpieqvd  26326  xrlimcnp  26463  cxploglim  26472  ftalem2  26568  ftalem7  26573  isppw2  26609  dchrptlem1  26757  dchrptlem3  26759  dchrsum2  26761  lgsdchrval  26847  lgsdchr  26848  gausslemma2dlem1a  26858  lgsquadlem1  26873  2lgsoddprmlem2  26902  dchrisumlem3  26984  dchrisum0fno1  27004  pntlem3  27102  pntleml  27104  ostth3  27131  nosupno  27196  nosupbday  27198  noinfbday  27213  scutun12  27301  oldssmade  27362  addsproplem2  27444  addsuniflem  27474  negsid  27505  negsunif  27519  precsexlem6  27648  precsexlem7  27649  precsexlem11  27653  brcgr  28148  brbtwn2  28153  axbtwnid  28187  axcontlem7  28218  usgrnloopALT  28450  uhgrspansubgrlem  28537  nbuhgr  28590  nbupgr  28591  wwlksnextprop  29156  elwspths2on  29204  erclwwlktr  29265  clwwlknscsh  29305  erclwwlkntr  29314  hashecclwwlkn1  29320  umgrhashecclwwlk  29321  3cyclfrgrrn1  29528  frgrregorufr  29568  frgr2wwlk1  29572  ubthlem1  30111  ubthlem3  30113  htthlem  30158  omlsii  30644  spansncol  30809  nmopun  31255  nmcexi  31267  riesz1  31306  elpjrn  31431  cvcon3  31525  chcv1  31596  atcvatlem  31626  chirredi  31635  br8d  31827  xrge0tsmsd  32197  ordtrest2NEWlem  32891  lmxrge0  32921  esumfsup  33057  esumpcvgval  33065  measdivcstALTV  33212  eulerpartlemgh  33366  dstfrvunirn  33462  afsval  33672  erdszelem8  34178  erdszelem11  34181  erdsze2lem2  34184  connpconn  34215  sconnpi1  34219  cvmsss2  34254  cvmfolem  34259  cvmliftmolem2  34262  cvmliftlem15  34278  cvmlift2lem1  34282  cvmlift3lem4  34302  cvmlift3lem5  34303  satfdmlem  34348  fmla1  34367  gonarlem  34374  gonar  34375  goalrlem  34376  goalr  34377  fmla0disjsuc  34378  fmlasucdisj  34379  satffunlem1lem1  34382  satffunlem1lem2  34383  satffunlem2lem1  34384  mrsub0  34496  mrsubcn  34499  msubrn  34509  msubvrs  34540  br8  34715  br6  34716  br4  34717  cgrtriv  34963  btwntriv2  34973  btwncomim  34974  btwnswapid  34978  btwnintr  34980  btwnexch3  34981  btwnouttr2  34983  ifscgr  35005  cgrxfr  35016  btwnxfr  35017  btwnconn3  35064  segcon2  35066  brsegle  35069  seglecgr12im  35071  broutsideof3  35087  linethru  35114  elhf2  35136  opnregcld  35204  cldregopn  35205  neibastop2lem  35234  matunitlindflem1  36473  poimirlem16  36493  poimirlem17  36494  poimirlem19  36496  poimirlem20  36497  poimirlem24  36501  poimirlem29  36506  heicant  36512  opnmbllem0  36513  ismblfin  36518  itg2addnclem  36528  itg2addnclem3  36530  itg2gt0cn  36532  ftc1anclem5  36554  ftc2nc  36559  filbcmb  36597  fdc  36602  incsequz  36605  caushft  36618  istotbnd3  36628  equivbnd  36647  cntotbnd  36653  heibor1lem  36666  heibor1  36667  bfplem2  36680  divrngidl  36885  prnc  36924  lshpdisj  37846  cvrcon3b  38136  atnle  38176  hlhgt2  38249  hl0lt1N  38250  hl2at  38265  cvrexchlem  38279  cvratlem  38281  lvolnlelpln  38445  2lplnj  38480  ispsubcl2N  38807  lautcvr  38952  dva1dim  39845  dib1dim  40025  dib1dim2  40028  diclspsn  40054  dih1dimatlem  40189  dihlatat  40197  dihatexv  40198  dihatexv2  40199  lcfrlem9  40410  lcfrlem16  40418  mapdrvallem2  40505  mapd1o  40508  elre0re  41173  dvdsexpim  41215  prjspner1  41365  dffltz  41373  rexlimdv3d  41407  elrfi  41418  isnacs3  41434  eldiophb  41481  eldiophss  41498  diophren  41537  rencldnfilem  41544  pell1234qrdich  41585  pellfundex  41610  lsmfgcl  41802  kercvrlsm  41811  lmhmfgima  41812  lpirlnr  41845  hbtlem2  41852  hbtlem4  41854  hbtlem6  41857  rngunsnply  41901  onexoegt  41979  oaabsb  42030  cantnfresb  42060  omabs2  42068  tfsconcatrev  42084  restuni3  43793  limsupubuz  44416  stoweidlem57  44760  fourierdlem48  44857  fourierdlem49  44858  sge0le  45110  fsetsniunop  45746  cfsetsnfsetfo  45757  fcoresf1  45766  euoreqb  45804  imasetpreimafvbijlemf1  46059  imasetpreimafvbijlemfo  46060  iccpartrn  46085  iccpartiun  46089  iccpartnel  46093  paireqne  46166  reupr  46177  odz2prm2pw  46218  fmtnofac2lem  46223  prmdvdsfmtnof1lem2  46240  2pwp1prm  46244  mod42tp1mod8  46257  lighneallem3  46262  lighneallem4  46265  requad01  46276  requad2  46278  fppr2odd  46386  gbowpos  46414  gbowgt5  46417  gboge9  46419  nnsum4primesodd  46451  nnsum4primesoddALTV  46452  isomushgr  46481  isomuspgrlem2d  46486  copisnmnd  46566  ring2idlqusb  46776  lidldomn1  46777  affinecomb1  47342  eenglngeehlnmlem2  47378  rrx2vlinest  47381  itsclquadb  47416  rspceb2dv  47442  aacllem  47802