Theorem rexlimdva 3152

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-rex 3068

This theorem is referenced by:  rexlimdvaa  3153  rexlimivv  3198  rexlimdvv  3209  rspceb2dv  3625  ssexnelpss  4125  ralxfrd2  5417  iunopeqop  5530  elsnxp  6312  foco2  7128  elunirn  7270  f1elima  7282  mptcnfimad  8009  releldmdifi  8068  mpoexw  8101  xpord3pred  8175  sexp3  8176  tfrlem9a  8424  seqomlem2  8489  oawordexr  8592  odi  8615  oelimcl  8636  nnawordex  8673  nnaordex  8674  oaabs  8684  oaabs2  8685  omabs  8687  eldifsucnn  8700  coflton  8707  cofon1  8708  cofon2  8709  cofonr  8710  naddunif  8729  ectocld  8822  onfin  9264  dif1ennnALT  9308  isfinite2  9331  isfiniteg  9334  fofinf1o  9369  elfiun  9467  suplub2  9498  supisoex  9511  ordtypelem9  9563  ordtypelem10  9564  brwdom2  9610  brwdom3  9619  ttrcltr  9753  rankr1ai  9835  fodomfi2  10097  infpwfien  10099  dfac12r  10184  ackbij1  10274  cff1  10295  fin23lem21  10376  isf32lem2  10391  fin1a2lem11  10447  fin1a2lem13  10449  ficard  10602  gchina  10736  eltsk2g  10788  tskr1om2  10805  rankcf  10814  inatsk  10815  tskuni  10820  nqereu  10966  ltexnq  11012  1idpr  11066  suplem1pr  11089  supsrlem  11148  axpre-sup  11206  1re  11258  0re  11260  0cnALT  11493  supaddc  12232  supadd  12233  supmul1  12234  supmul  12237  suprzcl2  12977  qmulz  12990  elpq  13014  qbtwnre  13237  ioo0  13408  ico0  13429  ioc0  13430  icc0  13431  addmodlteq  13983  fsequb  14012  hashdom  14414  ccats1alpha  14653  reuccatpfxs1lem  14780  shftlem  15103  rexuzre  15387  rexico  15388  caubnd  15393  limsupbnd1  15514  limsupbnd2  15515  rlim2lt  15529  rlim3  15530  lo1bdd2  15556  lo1bddrp  15557  o1lo1  15569  climuni  15584  climshftlem  15606  o1co  15618  rlimcn1  15620  climcn1  15624  o1rlimmul  15651  lo1le  15684  rlimno1  15686  isercoll  15700  caurcvg2  15710  serf0  15713  summolem2  15748  zsum  15750  fsum2dlem  15802  geomulcvg  15908  mertenslem2  15917  ntrivcvg  15929  zprod  15969  fprod2dlem  16012  dvds1lem  16301  dvdsexp2im  16360  odd2np1lem  16373  sqoddm1div8z  16387  ltoddhalfle  16394  halfleoddlt  16395  flodddiv4  16448  dvdssqim  16587  dvdsexpim  16588  coprmdvds2  16687  divgcdcoprm0  16698  cncongr1  16700  cncongr2  16701  isprm5  16740  rpexp  16755  pythagtriplem1  16849  iserodd  16868  pc2dvds  16912  difsqpwdvds  16920  oddprmdvds  16936  prmpwdvds  16937  4sqlem11  16988  vdwapun  17007  vdwlem2  17015  vdwlem6  17019  vdwlem8  17021  vdwlem10  17023  vdwnnlem1  17028  vdwnnlem3  17030  0ram  17053  ramub1lem2  17060  ramcl  17062  cshwsiun  17133  cshwrepswhash1  17136  firest  17478  imasvscafn  17583  imasmnd2  18799  dfgrp3lem  19068  imasgrp2  19085  issubg4  19175  cycsubm  19232  gaorber  19338  orbsta  19343  pmtr3ncom  19507  psgnran  19547  odmulg  19588  odbezout  19590  gexdvdsi  19615  sylow1lem3  19632  odcau  19636  sylow2alem1  19649  sylow3lem6  19664  lsmelvalm  19683  efgrelexlemb  19782  efgredeu  19784  imasabl  19908  cyggeninv  19915  cygctb  19924  cyggexb  19931  dprdssv  20050  dprddisj2  20073  ablfacrplem  20099  pgpfac1lem2  20109  pgpfac1lem5  20113  ringinvnzdiv  20314  imasring  20343  dvdsrcl2  20382  dvdsrmul1  20385  lss1d  20978  lssats2  21015  lspsn  21017  lmhmima  21063  ring2idlqusb  21337  rngqiprngfulem2  21339  lpiss  21356  dvdsrzring  21489  pzriprnglem5  21513  pzriprnglem8  21516  pzriprnglem10  21518  pzriprnglem11  21519  znunit  21599  znrrg  21601  cygznlem3  21605  frgpcyg  21609  lindfrn  21858  mplcoe5lem  22074  mpfind  22148  gsummoncoe1  22327  mpfpf1  22370  pf1mpf  22371  mat1dimelbas  22492  scmatdmat  22536  scmataddcl  22537  scmatsubcl  22538  scmatmulcl  22539  cpmatacl  22737  chpscmat  22863  tgcl  22991  clsval2  23073  innei  23148  restcld  23195  restcldr  23197  ordtrest2lem  23226  cnprest  23312  lmss  23321  lmcls  23325  lmcnp  23327  isreg2  23400  cmpcovf  23414  cncmp  23415  cmpsub  23423  1stcrest  23476  2ndcrest  23477  1stccnp  23485  restnlly  23505  cldllycmp  23518  locfincmp  23549  txcnpi  23631  pthaus  23661  txtube  23663  txcmplem1  23664  txcmplem2  23665  txlm  23671  xkohaus  23676  xkococnlem  23682  xkococn  23683  kqfvima  23753  kqreglem1  23764  isfild  23881  filuni  23908  isufil2  23931  uffix  23944  rnelfm  23976  fmfnfmlem2  23978  fmfnfmlem4  23980  fmfnfm  23981  fmco  23984  fclsopn  24037  ufilcmp  24055  cnpfcf  24064  alexsublem  24067  alexsubALT  24074  cldsubg  24134  ghmcnp  24138  qustgpopn  24143  tsmsgsum  24162  tsmsres  24167  tsmsxplem1  24176  tsmsxp  24178  isucn2  24303  ucnprima  24306  imasdsf1olem  24398  blssps  24449  blss  24450  blssexps  24451  blssex  24452  mopni3  24522  blcld  24533  metrest  24552  metcnp3  24568  reperflem  24853  icccmplem3  24859  xrge0tsms  24869  mulc1cncf  24944  cncfco  24946  cnheibor  25000  bndth  25003  lebnumlem3  25008  xlebnum  25010  lebnumii  25011  nmhmcn  25166  cfil3i  25316  cmetcaulem  25335  cfilres  25343  bcthlem4  25374  ivthlem2  25500  ivthlem3  25501  ivthicc  25506  cniccbdd  25509  ovolunlem1  25545  ovoliunlem2  25551  ovolshftlem2  25558  ovolicc2  25570  iunmbl2  25605  dyadmax  25646  opnmbllem  25649  subopnmbl  25652  volivth  25655  ismbf3d  25702  mbfimaopn2  25705  mbfaddlem  25708  i1fmullem  25742  mbfi1fseqlem4  25767  bddiblnc  25891  ellimc3  25928  dvlip  26046  dvlip2  26048  c1liplem1  26049  dvgt0lem1  26055  dvivthlem2  26062  dvne0  26064  lhop1lem  26066  lhop2  26068  lhop  26069  tdeglem4  26113  mdegnn0cl  26124  ply1divex  26190  dvdsq1p  26216  ig1peu  26228  elply2  26249  plypf1  26265  plydivex  26353  aalioulem3  26390  aalioulem5  26392  aaliou  26394  ulmshftlem  26446  ulmcau  26452  ulmss  26454  ulmbdd  26455  ulmcn  26456  radcnvlt1  26475  eflogeq  26658  efopn  26714  cxpeq  26814  angpieqvd  26888  xrlimcnp  27025  cxploglim  27035  ftalem2  27131  ftalem7  27136  isppw2  27172  dchrptlem1  27322  dchrptlem3  27324  dchrsum2  27326  lgsdchrval  27412  lgsdchr  27413  gausslemma2dlem1a  27423  lgsquadlem1  27438  2lgsoddprmlem2  27467  dchrisumlem3  27549  dchrisum0fno1  27569  pntlem3  27667  pntleml  27669  ostth3  27696  nosupno  27762  nosupbday  27764  noinfbday  27779  scutun12  27869  oldssmade  27930  addsproplem2  28017  addsuniflem  28048  addsbdaylem  28063  negsid  28087  negsunif  28101  precsexlem6  28250  precsexlem7  28251  precsexlem11  28255  onaddscl  28300  om2noseqlt  28319  noseqrdgfn  28326  dfnns2  28376  zs12bday  28438  recut  28442  brcgr  28929  brbtwn2  28934  axbtwnid  28968  axcontlem7  28999  usgrnloopALT  29234  uhgrspansubgrlem  29321  nbuhgr  29374  nbupgr  29375  wwlksnextprop  29941  elwspths2on  29989  erclwwlktr  30050  clwwlknscsh  30090  erclwwlkntr  30099  hashecclwwlkn1  30105  umgrhashecclwwlk  30106  3cyclfrgrrn1  30313  frgrregorufr  30353  frgr2wwlk1  30357  ubthlem1  30898  ubthlem3  30900  htthlem  30945  omlsii  31431  spansncol  31596  nmopun  32042  nmcexi  32054  riesz1  32093  elpjrn  32218  cvcon3  32312  chcv1  32383  atcvatlem  32413  chirredi  32422  br8d  32629  xrge0tsmsd  33047  ordtrest2NEWlem  33882  lmxrge0  33912  esumfsup  34050  esumpcvgval  34058  measdivcstALTV  34205  eulerpartlemgh  34359  dstfrvunirn  34455  afsval  34664  erdszelem8  35182  erdszelem11  35185  erdsze2lem2  35188  connpconn  35219  sconnpi1  35223  cvmsss2  35258  cvmfolem  35263  cvmliftmolem2  35266  cvmliftlem15  35282  cvmlift2lem1  35286  cvmlift3lem4  35306  cvmlift3lem5  35307  satfdmlem  35352  fmla1  35371  gonarlem  35378  gonar  35379  goalrlem  35380  goalr  35381  fmla0disjsuc  35382  fmlasucdisj  35383  satffunlem1lem1  35386  satffunlem1lem2  35387  satffunlem2lem1  35388  mrsub0  35500  mrsubcn  35503  msubrn  35513  msubvrs  35544  br8  35735  br6  35736  br4  35737  cgrtriv  35983  btwntriv2  35993  btwncomim  35994  btwnswapid  35998  btwnintr  36000  btwnexch3  36001  btwnouttr2  36003  ifscgr  36025  cgrxfr  36036  btwnxfr  36037  btwnconn3  36084  segcon2  36086  brsegle  36089  seglecgr12im  36091  broutsideof3  36107  linethru  36134  elhf2  36156  opnregcld  36312  cldregopn  36313  neibastop2lem  36342  matunitlindflem1  37602  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem24  37630  poimirlem29  37635  heicant  37641  opnmbllem0  37642  ismblfin  37647  itg2addnclem  37657  itg2addnclem3  37659  itg2gt0cn  37661  ftc1anclem5  37683  ftc2nc  37688  filbcmb  37726  fdc  37731  incsequz  37734  caushft  37747  istotbnd3  37757  equivbnd  37776  cntotbnd  37782  heibor1lem  37795  heibor1  37796  bfplem2  37809  divrngidl  38014  prnc  38053  lshpdisj  38968  cvrcon3b  39258  atnle  39298  hlhgt2  39371  hl0lt1N  39372  hl2at  39387  cvrexchlem  39401  cvratlem  39403  lvolnlelpln  39567  2lplnj  39602  ispsubcl2N  39929  lautcvr  40074  dva1dim  40967  dib1dim  41147  dib1dim2  41150  diclspsn  41176  dih1dimatlem  41311  dihlatat  41319  dihatexv  41320  dihatexv2  41321  lcfrlem9  41532  lcfrlem16  41540  mapdrvallem2  41627  mapd1o  41630  aks6d1c2  42111  elre0re  42273  prjspner1  42612  dffltz  42620  rexlimdv3d  42670  elrfi  42681  isnacs3  42697  eldiophb  42744  eldiophss  42761  diophren  42800  rencldnfilem  42807  pell1234qrdich  42848  pellfundex  42873  lsmfgcl  43062  kercvrlsm  43071  lmhmfgima  43072  lpirlnr  43105  hbtlem2  43112  hbtlem4  43114  hbtlem6  43117  rngunsnply  43157  onexoegt  43232  oaabsb  43283  cantnfresb  43313  omabs2  43321  tfsconcatrev  43337  restuni3  45057  limsupubuz  45668  stoweidlem57  46012  fourierdlem48  46109  fourierdlem49  46110  sge0le  46362  fsetsniunop  46998  cfsetsnfsetfo  47009  fcoresf1  47018  euoreqb  47058  imasetpreimafvbijlemf1  47328  imasetpreimafvbijlemfo  47329  iccpartrn  47354  iccpartiun  47358  iccpartnel  47362  paireqne  47435  reupr  47446  odz2prm2pw  47487  fmtnofac2lem  47492  prmdvdsfmtnof1lem2  47509  2pwp1prm  47513  mod42tp1mod8  47526  lighneallem3  47531  lighneallem4  47534  requad01  47545  requad2  47547  fppr2odd  47655  gbowpos  47683  gbowgt5  47686  gboge9  47688  nnsum4primesodd  47720  nnsum4primesoddALTV  47721  isubgredg  47789  isuspgrim0  47809  isuspgrimlem  47811  grimcnv  47816  gricushgr  47823  clnbgrgrimlem  47838  clnbgrgrim  47839  grimedg  47840  grtrissvtx  47848  stgrusgra  47861  isubgr3stgrlem7  47874  gpgedgel  47942  gpgusgralem  47945  gpgvtxedg0  47955  gpgvtxedg1  47956  copisnmnd  48012  lidldomn1  48074  affinecomb1  48551  eenglngeehlnmlem2  48587  rrx2vlinest  48590  itsclquadb  48625  aacllem  49031