Theorem rexlimdva 3151

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2099  ∃wrex 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-rex 3067

This theorem is referenced by:  rexlimdvaa  3152  rexlimivv  3195  rexlimdvv  3206  rspceb2dv  3612  ssexnelpss  4110  ralxfrd2  5407  iunopeqop  5518  elsnxp  6290  foco2  7114  elunirn  7256  f1elima  7268  mptcnfimad  7985  releldmdifi  8044  mpoexw  8078  xpord3pred  8152  sexp3  8153  tfrlem9a  8401  seqomlem2  8466  oawordexr  8571  odi  8594  oelimcl  8615  nnawordex  8652  nnaordex  8653  oaabs  8663  oaabs2  8664  omabs  8666  eldifsucnn  8679  coflton  8686  cofon1  8687  cofon2  8688  cofonr  8689  naddunif  8708  ectocld  8797  onfin  9249  dif1ennnALT  9296  isfinite2  9320  isfiniteg  9323  fofinf1o  9346  elfiun  9448  suplub2  9479  supisoex  9492  ordtypelem9  9544  ordtypelem10  9545  brwdom2  9591  brwdom3  9600  ttrcltr  9734  rankr1ai  9816  fodomfi2  10078  infpwfien  10080  dfac12r  10164  ackbij1  10256  cff1  10276  fin23lem21  10357  isf32lem2  10372  fin1a2lem11  10428  fin1a2lem13  10430  ficard  10583  gchina  10717  eltsk2g  10769  tskr1om2  10786  rankcf  10795  inatsk  10796  tskuni  10801  nqereu  10947  ltexnq  10993  1idpr  11047  suplem1pr  11070  supsrlem  11129  axpre-sup  11187  1re  11239  0re  11241  0cnALT  11473  negfi  12188  supaddc  12206  supadd  12207  supmul1  12208  supmul  12211  suprzcl2  12947  qmulz  12960  elpq  12984  qbtwnre  13205  ioo0  13376  ico0  13397  ioc0  13398  icc0  13399  addmodlteq  13938  fsequb  13967  hashdom  14365  ccats1alpha  14596  reuccatpfxs1lem  14723  shftlem  15042  rexuzre  15326  rexico  15327  caubnd  15332  limsupbnd1  15453  limsupbnd2  15454  rlim2lt  15468  rlim3  15469  lo1bdd2  15495  lo1bddrp  15496  o1lo1  15508  climuni  15523  climshftlem  15545  o1co  15557  rlimcn1  15559  climcn1  15563  o1rlimmul  15590  lo1le  15625  rlimno1  15627  isercoll  15641  caurcvg2  15651  serf0  15654  summolem2  15689  zsum  15691  fsum2dlem  15743  geomulcvg  15849  mertenslem2  15858  ntrivcvg  15870  zprod  15908  fprod2dlem  15951  dvds1lem  16239  dvdsexp2im  16298  odd2np1lem  16311  sqoddm1div8z  16325  ltoddhalfle  16332  halfleoddlt  16333  flodddiv4  16384  dvdssqim  16524  coprmdvds2  16619  divgcdcoprm0  16630  cncongr1  16632  cncongr2  16633  isprm5  16672  rpexp  16688  pythagtriplem1  16779  iserodd  16798  pc2dvds  16842  difsqpwdvds  16850  oddprmdvds  16866  prmpwdvds  16867  4sqlem11  16918  vdwapun  16937  vdwlem2  16945  vdwlem6  16949  vdwlem8  16951  vdwlem10  16953  vdwnnlem1  16958  vdwnnlem3  16960  0ram  16983  ramub1lem2  16990  ramcl  16992  cshwsiun  17063  cshwrepswhash1  17066  firest  17408  imasvscafn  17513  imasmnd2  18725  dfgrp3lem  18988  imasgrp2  19005  issubg4  19094  cycsubm  19151  gaorber  19253  orbsta  19258  pmtr3ncom  19424  psgnran  19464  odmulg  19505  odbezout  19507  gexdvdsi  19532  sylow1lem3  19549  odcau  19553  sylow2alem1  19566  sylow3lem6  19581  lsmelvalm  19600  efgrelexlemb  19699  efgredeu  19701  imasabl  19825  cyggeninv  19832  cygctb  19841  cyggexb  19848  dprdssv  19967  dprddisj2  19990  ablfacrplem  20016  pgpfac1lem2  20026  pgpfac1lem5  20030  ringinvnzdiv  20231  imasring  20260  dvdsrcl2  20299  dvdsrmul1  20302  lss1d  20841  lssats2  20878  lspsn  20880  lmhmima  20926  ring2idlqusb  21194  rngqiprngfulem2  21196  lpiss  21213  dvdsrzring  21381  pzriprnglem5  21405  pzriprnglem8  21408  pzriprnglem10  21410  pzriprnglem11  21411  znunit  21491  znrrg  21493  cygznlem3  21497  frgpcyg  21501  lindfrn  21749  mplcoe5lem  21971  mpfind  22047  gsummoncoe1  22221  mpfpf1  22264  pf1mpf  22265  mat1dimelbas  22367  scmatdmat  22411  scmataddcl  22412  scmatsubcl  22413  scmatmulcl  22414  cpmatacl  22612  chpscmat  22738  tgcl  22866  clsval2  22948  innei  23023  restcld  23070  restcldr  23072  ordtrest2lem  23101  cnprest  23187  lmss  23196  lmcls  23200  lmcnp  23202  isreg2  23275  cmpcovf  23289  cncmp  23290  cmpsub  23298  1stcrest  23351  2ndcrest  23352  1stccnp  23360  restnlly  23380  cldllycmp  23393  locfincmp  23424  txcnpi  23506  pthaus  23536  txtube  23538  txcmplem1  23539  txcmplem2  23540  txlm  23546  xkohaus  23551  xkococnlem  23557  xkococn  23558  kqfvima  23628  kqreglem1  23639  isfild  23756  filuni  23783  isufil2  23806  uffix  23819  rnelfm  23851  fmfnfmlem2  23853  fmfnfmlem4  23855  fmfnfm  23856  fmco  23859  fclsopn  23912  ufilcmp  23930  cnpfcf  23939  alexsublem  23942  alexsubALT  23949  cldsubg  24009  ghmcnp  24013  qustgpopn  24018  tsmsgsum  24037  tsmsres  24042  tsmsxplem1  24051  tsmsxp  24053  isucn2  24178  ucnprima  24181  imasdsf1olem  24273  blssps  24324  blss  24325  blssexps  24326  blssex  24327  mopni3  24397  blcld  24408  metrest  24427  metcnp3  24443  reperflem  24728  icccmplem3  24734  xrge0tsms  24744  mulc1cncf  24819  cncfco  24821  cnheibor  24875  bndth  24878  lebnumlem3  24883  xlebnum  24885  lebnumii  24886  nmhmcn  25041  cfil3i  25191  cmetcaulem  25210  cfilres  25218  bcthlem4  25249  ivthlem2  25375  ivthlem3  25376  ivthicc  25381  cniccbdd  25384  ovolunlem1  25420  ovoliunlem2  25426  ovolshftlem2  25433  ovolicc2  25445  iunmbl2  25480  dyadmax  25521  opnmbllem  25524  subopnmbl  25527  volivth  25530  ismbf3d  25577  mbfimaopn2  25580  mbfaddlem  25583  i1fmullem  25617  mbfi1fseqlem4  25642  bddiblnc  25765  ellimc3  25802  dvlip  25920  dvlip2  25922  c1liplem1  25923  dvgt0lem1  25929  dvivthlem2  25936  dvne0  25938  lhop1lem  25940  lhop2  25942  lhop  25943  tdeglem4  25989  tdeglem4OLD  25990  mdegnn0cl  26001  ply1divex  26066  dvdsq1p  26091  ig1peu  26103  elply2  26124  plypf1  26140  plydivex  26226  aalioulem3  26263  aalioulem5  26265  aaliou  26267  ulmshftlem  26319  ulmcau  26325  ulmss  26327  ulmbdd  26328  ulmcn  26329  radcnvlt1  26348  eflogeq  26530  efopn  26586  cxpeq  26686  angpieqvd  26757  xrlimcnp  26894  cxploglim  26904  ftalem2  27000  ftalem7  27005  isppw2  27041  dchrptlem1  27191  dchrptlem3  27193  dchrsum2  27195  lgsdchrval  27281  lgsdchr  27282  gausslemma2dlem1a  27292  lgsquadlem1  27307  2lgsoddprmlem2  27336  dchrisumlem3  27418  dchrisum0fno1  27438  pntlem3  27536  pntleml  27538  ostth3  27565  nosupno  27630  nosupbday  27632  noinfbday  27647  scutun12  27737  oldssmade  27798  addsproplem2  27881  addsuniflem  27912  negsid  27947  negsunif  27961  precsexlem6  28104  precsexlem7  28105  precsexlem11  28109  om2noseqlt  28166  noseqrdgfn  28173  recut  28218  brcgr  28705  brbtwn2  28710  axbtwnid  28744  axcontlem7  28775  usgrnloopALT  29010  uhgrspansubgrlem  29097  nbuhgr  29150  nbupgr  29151  wwlksnextprop  29717  elwspths2on  29765  erclwwlktr  29826  clwwlknscsh  29866  erclwwlkntr  29875  hashecclwwlkn1  29881  umgrhashecclwwlk  29882  3cyclfrgrrn1  30089  frgrregorufr  30129  frgr2wwlk1  30133  ubthlem1  30674  ubthlem3  30676  htthlem  30721  omlsii  31207  spansncol  31372  nmopun  31818  nmcexi  31830  riesz1  31869  elpjrn  31994  cvcon3  32088  chcv1  32159  atcvatlem  32189  chirredi  32198  br8d  32394  xrge0tsmsd  32766  ordtrest2NEWlem  33518  lmxrge0  33548  esumfsup  33684  esumpcvgval  33692  measdivcstALTV  33839  eulerpartlemgh  33993  dstfrvunirn  34089  afsval  34298  erdszelem8  34803  erdszelem11  34806  erdsze2lem2  34809  connpconn  34840  sconnpi1  34844  cvmsss2  34879  cvmfolem  34884  cvmliftmolem2  34887  cvmliftlem15  34903  cvmlift2lem1  34907  cvmlift3lem4  34927  cvmlift3lem5  34928  satfdmlem  34973  fmla1  34992  gonarlem  34999  gonar  35000  goalrlem  35001  goalr  35002  fmla0disjsuc  35003  fmlasucdisj  35004  satffunlem1lem1  35007  satffunlem1lem2  35008  satffunlem2lem1  35009  mrsub0  35121  mrsubcn  35124  msubrn  35134  msubvrs  35165  br8  35345  br6  35346  br4  35347  cgrtriv  35593  btwntriv2  35603  btwncomim  35604  btwnswapid  35608  btwnintr  35610  btwnexch3  35611  btwnouttr2  35613  ifscgr  35635  cgrxfr  35646  btwnxfr  35647  btwnconn3  35694  segcon2  35696  brsegle  35699  seglecgr12im  35701  broutsideof3  35717  linethru  35744  elhf2  35766  opnregcld  35809  cldregopn  35810  neibastop2lem  35839  matunitlindflem1  37084  poimirlem16  37104  poimirlem17  37105  poimirlem19  37107  poimirlem20  37108  poimirlem24  37112  poimirlem29  37117  heicant  37123  opnmbllem0  37124  ismblfin  37129  itg2addnclem  37139  itg2addnclem3  37141  itg2gt0cn  37143  ftc1anclem5  37165  ftc2nc  37170  filbcmb  37208  fdc  37213  incsequz  37216  caushft  37229  istotbnd3  37239  equivbnd  37258  cntotbnd  37264  heibor1lem  37277  heibor1  37278  bfplem2  37291  divrngidl  37496  prnc  37535  lshpdisj  38454  cvrcon3b  38744  atnle  38784  hlhgt2  38857  hl0lt1N  38858  hl2at  38873  cvrexchlem  38887  cvratlem  38889  lvolnlelpln  39053  2lplnj  39088  ispsubcl2N  39415  lautcvr  39560  dva1dim  40453  dib1dim  40633  dib1dim2  40636  diclspsn  40662  dih1dimatlem  40797  dihlatat  40805  dihatexv  40806  dihatexv2  40807  lcfrlem9  41018  lcfrlem16  41026  mapdrvallem2  41113  mapd1o  41116  aks6d1c2  41596  elre0re  41827  dvdsexpim  41879  prjspner1  42041  dffltz  42049  rexlimdv3d  42094  elrfi  42105  isnacs3  42121  eldiophb  42168  eldiophss  42185  diophren  42224  rencldnfilem  42231  pell1234qrdich  42272  pellfundex  42297  lsmfgcl  42489  kercvrlsm  42498  lmhmfgima  42499  lpirlnr  42532  hbtlem2  42539  hbtlem4  42541  hbtlem6  42544  rngunsnply  42588  onexoegt  42663  oaabsb  42714  cantnfresb  42744  omabs2  42752  tfsconcatrev  42768  restuni3  44475  limsupubuz  45092  stoweidlem57  45436  fourierdlem48  45533  fourierdlem49  45534  sge0le  45786  fsetsniunop  46422  cfsetsnfsetfo  46433  fcoresf1  46442  euoreqb  46480  imasetpreimafvbijlemf1  46735  imasetpreimafvbijlemfo  46736  iccpartrn  46761  iccpartiun  46765  iccpartnel  46769  paireqne  46842  reupr  46853  odz2prm2pw  46894  fmtnofac2lem  46899  prmdvdsfmtnof1lem2  46916  2pwp1prm  46920  mod42tp1mod8  46933  lighneallem3  46938  lighneallem4  46941  requad01  46952  requad2  46954  fppr2odd  47062  gbowpos  47090  gbowgt5  47093  gboge9  47095  nnsum4primesodd  47127  nnsum4primesoddALTV  47128  isuspgrim0  47161  isuspgrimlem  47163  grimcnv  47168  gricushgr  47174  copisnmnd  47222  lidldomn1  47284  affinecomb1  47766  eenglngeehlnmlem2  47802  rrx2vlinest  47805  itsclquadb  47840  aacllem  48225