Theorem rexlimdva 3142

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∃wrex 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3062

This theorem is referenced by:  rexlimdvaa  3143  rexlimivv  3187  rexlimdvv  3201  rspceb2dv  3610  ssexnelpss  4096  ralxfrd2  5387  iunopeqop  5501  elsnxp  6285  foco2  7104  elunirn  7248  f1elima  7261  mptcnfimad  7990  releldmdifi  8049  mpoexw  8082  xpord3pred  8156  sexp3  8157  tfrlem9a  8405  seqomlem2  8470  oawordexr  8573  odi  8596  oelimcl  8617  nnawordex  8654  nnaordex  8655  oaabs  8665  oaabs2  8666  omabs  8668  eldifsucnn  8681  coflton  8688  cofon1  8689  cofon2  8690  cofonr  8691  naddunif  8710  ectocld  8803  onfin  9244  dif1ennnALT  9288  isfinite2  9311  isfiniteg  9314  fofinf1o  9349  elfiun  9447  suplub2  9478  supisoex  9492  ordtypelem9  9545  ordtypelem10  9546  brwdom2  9592  brwdom3  9601  ttrcltr  9735  rankr1ai  9817  fodomfi2  10079  infpwfien  10081  dfac12r  10166  ackbij1  10256  cff1  10277  fin23lem21  10358  isf32lem2  10373  fin1a2lem11  10429  fin1a2lem13  10431  ficard  10584  gchina  10718  eltsk2g  10770  tskr1om2  10787  rankcf  10796  inatsk  10797  tskuni  10802  nqereu  10948  ltexnq  10994  1idpr  11048  suplem1pr  11071  supsrlem  11130  axpre-sup  11188  1re  11240  0re  11242  0cnALT  11475  supaddc  12214  supadd  12215  supmul1  12216  supmul  12219  suprzcl2  12959  qmulz  12972  elpq  12996  qbtwnre  13220  ioo0  13392  ico0  13413  ioc0  13414  icc0  13415  addmodlteq  13969  fsequb  13998  hashdom  14402  ccats1alpha  14642  reuccatpfxs1lem  14769  shftlem  15092  rexuzre  15376  rexico  15377  caubnd  15382  limsupbnd1  15503  limsupbnd2  15504  rlim2lt  15518  rlim3  15519  lo1bdd2  15545  lo1bddrp  15546  o1lo1  15558  climuni  15573  climshftlem  15595  o1co  15607  rlimcn1  15609  climcn1  15613  o1rlimmul  15640  lo1le  15673  rlimno1  15675  isercoll  15689  caurcvg2  15699  serf0  15702  summolem2  15737  zsum  15739  fsum2dlem  15791  geomulcvg  15897  mertenslem2  15906  ntrivcvg  15918  zprod  15958  fprod2dlem  16001  dvds1lem  16292  dvdsexp2im  16351  odd2np1lem  16364  sqoddm1div8z  16378  ltoddhalfle  16385  halfleoddlt  16386  flodddiv4  16439  dvdssqim  16578  dvdsexpim  16579  coprmdvds2  16678  divgcdcoprm0  16689  cncongr1  16691  cncongr2  16692  isprm5  16731  rpexp  16746  pythagtriplem1  16841  iserodd  16860  pc2dvds  16904  difsqpwdvds  16912  oddprmdvds  16928  prmpwdvds  16929  4sqlem11  16980  vdwapun  16999  vdwlem2  17007  vdwlem6  17011  vdwlem8  17013  vdwlem10  17015  vdwnnlem1  17020  vdwnnlem3  17022  0ram  17045  ramub1lem2  17052  ramcl  17054  cshwsiun  17124  cshwrepswhash1  17127  firest  17451  imasvscafn  17556  imasmnd2  18757  dfgrp3lem  19026  imasgrp2  19043  issubg4  19133  cycsubm  19190  gaorber  19296  orbsta  19301  pmtr3ncom  19461  psgnran  19501  odmulg  19542  odbezout  19544  gexdvdsi  19569  sylow1lem3  19586  odcau  19590  sylow2alem1  19603  sylow3lem6  19618  lsmelvalm  19637  efgrelexlemb  19736  efgredeu  19738  imasabl  19862  cyggeninv  19869  cygctb  19878  cyggexb  19885  dprdssv  20004  dprddisj2  20027  ablfacrplem  20053  pgpfac1lem2  20063  pgpfac1lem5  20067  ringinvnzdiv  20266  imasring  20295  dvdsrcl2  20331  dvdsrmul1  20334  lss1d  20925  lssats2  20962  lspsn  20964  lmhmima  21010  ring2idlqusb  21276  rngqiprngfulem2  21278  lpiss  21295  dvdsrzring  21427  pzriprnglem5  21451  pzriprnglem8  21454  pzriprnglem10  21456  pzriprnglem11  21457  znunit  21529  znrrg  21531  cygznlem3  21535  frgpcyg  21539  lindfrn  21786  mplcoe5lem  22002  mpfind  22070  gsummoncoe1  22251  mpfpf1  22294  pf1mpf  22295  mat1dimelbas  22414  scmatdmat  22458  scmataddcl  22459  scmatsubcl  22460  scmatmulcl  22461  cpmatacl  22659  chpscmat  22785  tgcl  22912  clsval2  22993  innei  23068  restcld  23115  restcldr  23117  ordtrest2lem  23146  cnprest  23232  lmss  23241  lmcls  23245  lmcnp  23247  isreg2  23320  cmpcovf  23334  cncmp  23335  cmpsub  23343  1stcrest  23396  2ndcrest  23397  1stccnp  23405  restnlly  23425  cldllycmp  23438  locfincmp  23469  txcnpi  23551  pthaus  23581  txtube  23583  txcmplem1  23584  txcmplem2  23585  txlm  23591  xkohaus  23596  xkococnlem  23602  xkococn  23603  kqfvima  23673  kqreglem1  23684  isfild  23801  filuni  23828  isufil2  23851  uffix  23864  rnelfm  23896  fmfnfmlem2  23898  fmfnfmlem4  23900  fmfnfm  23901  fmco  23904  fclsopn  23957  ufilcmp  23975  cnpfcf  23984  alexsublem  23987  alexsubALT  23994  cldsubg  24054  ghmcnp  24058  qustgpopn  24063  tsmsgsum  24082  tsmsres  24087  tsmsxplem1  24096  tsmsxp  24098  isucn2  24222  ucnprima  24225  imasdsf1olem  24317  blssps  24368  blss  24369  blssexps  24370  blssex  24371  mopni3  24438  blcld  24449  metrest  24468  metcnp3  24484  reperflem  24763  icccmplem3  24769  xrge0tsms  24779  mulc1cncf  24854  cncfco  24856  cnheibor  24910  bndth  24913  lebnumlem3  24918  xlebnum  24920  lebnumii  24921  nmhmcn  25076  cfil3i  25226  cmetcaulem  25245  cfilres  25253  bcthlem4  25284  ivthlem2  25410  ivthlem3  25411  ivthicc  25416  cniccbdd  25419  ovolunlem1  25455  ovoliunlem2  25461  ovolshftlem2  25468  ovolicc2  25480  iunmbl2  25515  dyadmax  25556  opnmbllem  25559  subopnmbl  25562  volivth  25565  ismbf3d  25612  mbfimaopn2  25615  mbfaddlem  25618  i1fmullem  25652  mbfi1fseqlem4  25676  bddiblnc  25800  ellimc3  25837  dvlip  25955  dvlip2  25957  c1liplem1  25958  dvgt0lem1  25964  dvivthlem2  25971  dvne0  25973  lhop1lem  25975  lhop2  25977  lhop  25978  tdeglem4  26022  mdegnn0cl  26033  ply1divex  26099  dvdsq1p  26125  ig1peu  26137  elply2  26158  plypf1  26174  plydivex  26262  aalioulem3  26299  aalioulem5  26301  aaliou  26303  ulmshftlem  26355  ulmcau  26361  ulmss  26363  ulmbdd  26364  ulmcn  26365  radcnvlt1  26384  eflogeq  26568  efopn  26624  cxpeq  26724  angpieqvd  26798  xrlimcnp  26935  cxploglim  26945  ftalem2  27041  ftalem7  27046  isppw2  27082  dchrptlem1  27232  dchrptlem3  27234  dchrsum2  27236  lgsdchrval  27322  lgsdchr  27323  gausslemma2dlem1a  27333  lgsquadlem1  27348  2lgsoddprmlem2  27377  dchrisumlem3  27459  dchrisum0fno1  27479  pntlem3  27577  pntleml  27579  ostth3  27606  nosupno  27672  nosupbday  27674  noinfbday  27689  scutun12  27779  oldssmade  27846  addsproplem2  27934  addsuniflem  27965  addsbdaylem  27980  negsid  28004  negsunif  28018  precsexlem6  28171  precsexlem7  28172  precsexlem11  28176  bdayon  28230  onaddscl  28231  om2noseqlt  28250  noseqrdgfn  28257  n0sfincut  28303  bdayn0sf1o  28316  dfnns2  28318  zs12negscl  28397  zs12bday  28400  recut  28404  brcgr  28884  brbtwn2  28889  axbtwnid  28923  axcontlem7  28954  usgrnloopALT  29187  uhgrspansubgrlem  29274  nbuhgr  29327  nbupgr  29328  wwlksnextprop  29899  elwspths2on  29947  erclwwlktr  30008  clwwlknscsh  30048  erclwwlkntr  30057  hashecclwwlkn1  30063  umgrhashecclwwlk  30064  3cyclfrgrrn1  30271  frgrregorufr  30311  frgr2wwlk1  30315  ubthlem1  30856  ubthlem3  30858  htthlem  30903  omlsii  31389  spansncol  31554  nmopun  32000  nmcexi  32012  riesz1  32051  elpjrn  32176  cvcon3  32270  chcv1  32341  atcvatlem  32371  chirredi  32380  br8d  32595  xrge0tsmsd  33061  ordtrest2NEWlem  33958  lmxrge0  33988  esumfsup  34106  esumpcvgval  34114  measdivcstALTV  34261  eulerpartlemgh  34415  dstfrvunirn  34512  afsval  34708  erdszelem8  35225  erdszelem11  35228  erdsze2lem2  35231  connpconn  35262  sconnpi1  35266  cvmsss2  35301  cvmfolem  35306  cvmliftmolem2  35309  cvmliftlem15  35325  cvmlift2lem1  35329  cvmlift3lem4  35349  cvmlift3lem5  35350  satfdmlem  35395  fmla1  35414  gonarlem  35421  gonar  35422  goalrlem  35423  goalr  35424  fmla0disjsuc  35425  fmlasucdisj  35426  satffunlem1lem1  35429  satffunlem1lem2  35430  satffunlem2lem1  35431  mrsub0  35543  mrsubcn  35546  msubrn  35556  msubvrs  35587  br8  35778  br6  35779  br4  35780  cgrtriv  36025  btwntriv2  36035  btwncomim  36036  btwnswapid  36040  btwnintr  36042  btwnexch3  36043  btwnouttr2  36045  ifscgr  36067  cgrxfr  36078  btwnxfr  36079  btwnconn3  36126  segcon2  36128  brsegle  36131  seglecgr12im  36133  broutsideof3  36149  linethru  36176  elhf2  36198  opnregcld  36353  cldregopn  36354  neibastop2lem  36383  matunitlindflem1  37645  poimirlem16  37665  poimirlem17  37666  poimirlem19  37668  poimirlem20  37669  poimirlem24  37673  poimirlem29  37678  heicant  37684  opnmbllem0  37685  ismblfin  37690  itg2addnclem  37700  itg2addnclem3  37702  itg2gt0cn  37704  ftc1anclem5  37726  ftc2nc  37731  filbcmb  37769  fdc  37774  incsequz  37777  caushft  37790  istotbnd3  37800  equivbnd  37819  cntotbnd  37825  heibor1lem  37838  heibor1  37839  bfplem2  37852  divrngidl  38057  prnc  38096  lshpdisj  39010  cvrcon3b  39300  atnle  39340  hlhgt2  39413  hl0lt1N  39414  hl2at  39429  cvrexchlem  39443  cvratlem  39445  lvolnlelpln  39609  2lplnj  39644  ispsubcl2N  39971  lautcvr  40116  dva1dim  41009  dib1dim  41189  dib1dim2  41192  diclspsn  41218  dih1dimatlem  41353  dihlatat  41361  dihatexv  41362  dihatexv2  41363  lcfrlem9  41574  lcfrlem16  41582  mapdrvallem2  41669  mapd1o  41672  aks6d1c2  42148  elre0re  42272  prjspner1  42624  dffltz  42632  rexlimdv3d  42681  elrfi  42692  isnacs3  42708  eldiophb  42755  eldiophss  42772  diophren  42811  rencldnfilem  42818  pell1234qrdich  42859  pellfundex  42884  lsmfgcl  43073  kercvrlsm  43082  lmhmfgima  43083  lpirlnr  43116  hbtlem2  43123  hbtlem4  43125  hbtlem6  43128  rngunsnply  43168  onexoegt  43243  oaabsb  43293  cantnfresb  43323  omabs2  43331  tfsconcatrev  43347  restuni3  45122  limsupubuz  45722  stoweidlem57  46066  fourierdlem48  46163  fourierdlem49  46164  sge0le  46416  fsetsniunop  47058  cfsetsnfsetfo  47069  fcoresf1  47078  euoreqb  47118  imasetpreimafvbijlemf1  47398  imasetpreimafvbijlemfo  47399  iccpartrn  47424  iccpartiun  47428  iccpartnel  47432  paireqne  47505  reupr  47516  odz2prm2pw  47557  fmtnofac2lem  47562  prmdvdsfmtnof1lem2  47579  2pwp1prm  47583  mod42tp1mod8  47596  lighneallem3  47601  lighneallem4  47604  requad01  47615  requad2  47617  fppr2odd  47725  gbowpos  47753  gbowgt5  47756  gboge9  47758  nnsum4primesodd  47790  nnsum4primesoddALTV  47791  isubgredg  47859  grimcnv  47881  uhgrimedgi  47883  isuspgrim0  47887  isuspgrimlem  47888  gricushgr  47910  clnbgrgrimlem  47926  clnbgrgrim  47927  grimedg  47928  grtrissvtx  47936  stgrusgra  47951  isubgr3stgrlem7  47964  gpgiedgdmellem  48030  gpgusgralem  48040  gpgvtxedg0  48047  gpgvtxedg1  48048  copisnmnd  48124  lidldomn1  48186  affinecomb1  48662  eenglngeehlnmlem2  48698  rrx2vlinest  48701  itsclquadb  48736  aacllem  49645