Theorem rexlimdva 3134

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∃wrex 3057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3058

This theorem is referenced by:  rexlimdvaa  3135  rexlimivv  3175  rexlimdvv  3189  rspceb2dv  3577  ssexnelpss  4065  ralxfrd2  5352  iunopeqop  5464  elsnxp  6243  foco2  7048  elunirn  7191  f1elima  7203  mptcnfimad  7924  releldmdifi  7983  mpoexw  8016  xpord3pred  8088  sexp3  8089  tfrlem9a  8311  seqomlem2  8376  oawordexr  8477  odi  8500  oelimcl  8521  nnawordex  8558  nnaordex  8559  oaabs  8569  oaabs2  8570  omabs  8572  eldifsucnn  8585  coflton  8592  cofon1  8593  cofon2  8594  cofonr  8595  naddunif  8614  ectocld  8712  onfin  9131  dif1ennnALT  9168  isfinite2  9189  isfiniteg  9191  fofinf1o  9223  elfiun  9321  suplub2  9352  supisoex  9366  ordtypelem9  9419  ordtypelem10  9420  brwdom2  9466  brwdom3  9475  ttrcltr  9613  rankr1ai  9698  fodomfi2  9958  infpwfien  9960  dfac12r  10045  ackbij1  10135  cff1  10156  fin23lem21  10237  isf32lem2  10252  fin1a2lem11  10308  fin1a2lem13  10310  ficard  10463  gchina  10597  eltsk2g  10649  tskr1om2  10666  rankcf  10675  inatsk  10676  tskuni  10681  nqereu  10827  ltexnq  10873  1idpr  10927  suplem1pr  10950  supsrlem  11009  axpre-sup  11067  1re  11119  0re  11121  0cnALT  11355  supaddc  12096  supadd  12097  supmul1  12098  supmul  12101  suprzcl2  12838  qmulz  12851  elpq  12875  qbtwnre  13100  ioo0  13272  ico0  13293  ioc0  13294  icc0  13295  addmodlteq  13855  fsequb  13884  hashdom  14288  ccats1alpha  14529  reuccatpfxs1lem  14655  shftlem  14977  rexuzre  15262  rexico  15263  caubnd  15268  limsupbnd1  15391  limsupbnd2  15392  rlim2lt  15406  rlim3  15407  lo1bdd2  15433  lo1bddrp  15434  o1lo1  15446  climuni  15461  climshftlem  15483  o1co  15495  rlimcn1  15497  climcn1  15501  o1rlimmul  15528  lo1le  15561  rlimno1  15563  isercoll  15577  caurcvg2  15587  serf0  15590  summolem2  15625  zsum  15627  fsum2dlem  15679  geomulcvg  15785  mertenslem2  15794  ntrivcvg  15806  zprod  15846  fprod2dlem  15889  dvds1lem  16180  dvdsexp2im  16240  odd2np1lem  16253  sqoddm1div8z  16267  ltoddhalfle  16274  halfleoddlt  16275  flodddiv4  16328  dvdssqim  16467  dvdsexpim  16468  coprmdvds2  16567  divgcdcoprm0  16578  cncongr1  16580  cncongr2  16581  isprm5  16620  rpexp  16635  pythagtriplem1  16730  iserodd  16749  pc2dvds  16793  difsqpwdvds  16801  oddprmdvds  16817  prmpwdvds  16818  4sqlem11  16869  vdwapun  16888  vdwlem2  16896  vdwlem6  16900  vdwlem8  16902  vdwlem10  16904  vdwnnlem1  16909  vdwnnlem3  16911  0ram  16934  ramub1lem2  16941  ramcl  16943  cshwsiun  17013  cshwrepswhash1  17016  firest  17338  imasvscafn  17443  imasmnd2  18684  dfgrp3lem  18953  imasgrp2  18970  issubg4  19060  cycsubm  19116  gaorber  19222  orbsta  19227  pmtr3ncom  19389  psgnran  19429  odmulg  19470  odbezout  19472  gexdvdsi  19497  sylow1lem3  19514  odcau  19518  sylow2alem1  19531  sylow3lem6  19546  lsmelvalm  19565  efgrelexlemb  19664  efgredeu  19666  imasabl  19790  cyggeninv  19797  cygctb  19806  cyggexb  19813  dprdssv  19932  dprddisj2  19955  ablfacrplem  19981  pgpfac1lem2  19991  pgpfac1lem5  19995  ringinvnzdiv  20221  imasring  20250  dvdsrcl2  20286  dvdsrmul1  20289  lss1d  20898  lssats2  20935  lspsn  20937  lmhmima  20983  ring2idlqusb  21249  rngqiprngfulem2  21251  lpiss  21268  dvdsrzring  21400  pzriprnglem5  21424  pzriprnglem8  21427  pzriprnglem10  21429  pzriprnglem11  21430  znunit  21502  znrrg  21504  cygznlem3  21508  frgpcyg  21512  lindfrn  21760  mplcoe5lem  21975  mpfind  22043  gsummoncoe1  22224  mpfpf1  22267  pf1mpf  22268  mat1dimelbas  22387  scmatdmat  22431  scmataddcl  22432  scmatsubcl  22433  scmatmulcl  22434  cpmatacl  22632  chpscmat  22758  tgcl  22885  clsval2  22966  innei  23041  restcld  23088  restcldr  23090  ordtrest2lem  23119  cnprest  23205  lmss  23214  lmcls  23218  lmcnp  23220  isreg2  23293  cmpcovf  23307  cncmp  23308  cmpsub  23316  1stcrest  23369  2ndcrest  23370  1stccnp  23378  restnlly  23398  cldllycmp  23411  locfincmp  23442  txcnpi  23524  pthaus  23554  txtube  23556  txcmplem1  23557  txcmplem2  23558  txlm  23564  xkohaus  23569  xkococnlem  23575  xkococn  23576  kqfvima  23646  kqreglem1  23657  isfild  23774  filuni  23801  isufil2  23824  uffix  23837  rnelfm  23869  fmfnfmlem2  23871  fmfnfmlem4  23873  fmfnfm  23874  fmco  23877  fclsopn  23930  ufilcmp  23948  cnpfcf  23957  alexsublem  23960  alexsubALT  23967  cldsubg  24027  ghmcnp  24031  qustgpopn  24036  tsmsgsum  24055  tsmsres  24060  tsmsxplem1  24069  tsmsxp  24071  isucn2  24194  ucnprima  24197  imasdsf1olem  24289  blssps  24340  blss  24341  blssexps  24342  blssex  24343  mopni3  24410  blcld  24421  metrest  24440  metcnp3  24456  reperflem  24735  icccmplem3  24741  xrge0tsms  24751  mulc1cncf  24826  cncfco  24828  cnheibor  24882  bndth  24885  lebnumlem3  24890  xlebnum  24892  lebnumii  24893  nmhmcn  25048  cfil3i  25197  cmetcaulem  25216  cfilres  25224  bcthlem4  25255  ivthlem2  25381  ivthlem3  25382  ivthicc  25387  cniccbdd  25390  ovolunlem1  25426  ovoliunlem2  25432  ovolshftlem2  25439  ovolicc2  25451  iunmbl2  25486  dyadmax  25527  opnmbllem  25530  subopnmbl  25533  volivth  25536  ismbf3d  25583  mbfimaopn2  25586  mbfaddlem  25589  i1fmullem  25623  mbfi1fseqlem4  25647  bddiblnc  25771  ellimc3  25808  dvlip  25926  dvlip2  25928  c1liplem1  25929  dvgt0lem1  25935  dvivthlem2  25942  dvne0  25944  lhop1lem  25946  lhop2  25948  lhop  25949  tdeglem4  25993  mdegnn0cl  26004  ply1divex  26070  dvdsq1p  26096  ig1peu  26108  elply2  26129  plypf1  26145  plydivex  26233  aalioulem3  26270  aalioulem5  26272  aaliou  26274  ulmshftlem  26326  ulmcau  26332  ulmss  26334  ulmbdd  26335  ulmcn  26336  radcnvlt1  26355  eflogeq  26539  efopn  26595  cxpeq  26695  angpieqvd  26769  xrlimcnp  26906  cxploglim  26916  ftalem2  27012  ftalem7  27017  isppw2  27053  dchrptlem1  27203  dchrptlem3  27205  dchrsum2  27207  lgsdchrval  27293  lgsdchr  27294  gausslemma2dlem1a  27304  lgsquadlem1  27319  2lgsoddprmlem2  27348  dchrisumlem3  27430  dchrisum0fno1  27450  pntlem3  27548  pntleml  27550  ostth3  27577  nosupno  27643  nosupbday  27645  noinfbday  27660  scutun12  27752  oldssmade  27823  addsproplem2  27914  addsuniflem  27945  addsbdaylem  27960  negsid  27984  negsunif  27998  precsexlem6  28151  precsexlem7  28152  precsexlem11  28156  bdayon  28210  onaddscl  28211  om2noseqlt  28230  noseqrdgfn  28237  n0sfincut  28283  bdayn0sf1o  28296  dfnns2  28298  zs12negscl  28389  zs12zodd  28393  zs12bday  28395  recut  28399  brcgr  28880  brbtwn2  28885  axbtwnid  28919  axcontlem7  28950  usgrnloopALT  29183  uhgrspansubgrlem  29270  nbuhgr  29323  nbupgr  29324  wwlksnextprop  29892  elwspths2on  29942  elwspths2onw  29943  erclwwlktr  30004  clwwlknscsh  30044  erclwwlkntr  30053  hashecclwwlkn1  30059  umgrhashecclwwlk  30060  3cyclfrgrrn1  30267  frgrregorufr  30307  frgr2wwlk1  30311  ubthlem1  30852  ubthlem3  30854  htthlem  30899  omlsii  31385  spansncol  31550  nmopun  31996  nmcexi  32008  riesz1  32047  elpjrn  32172  cvcon3  32266  chcv1  32337  atcvatlem  32367  chirredi  32376  br8d  32593  xrge0tsmsd  33049  ordtrest2NEWlem  33956  lmxrge0  33986  esumfsup  34104  esumpcvgval  34112  measdivcstALTV  34259  eulerpartlemgh  34412  dstfrvunirn  34509  afsval  34705  onvf1odlem4  35171  erdszelem8  35263  erdszelem11  35266  erdsze2lem2  35269  connpconn  35300  sconnpi1  35304  cvmsss2  35339  cvmfolem  35344  cvmliftmolem2  35347  cvmliftlem15  35363  cvmlift2lem1  35367  cvmlift3lem4  35387  cvmlift3lem5  35388  satfdmlem  35433  fmla1  35452  gonarlem  35459  gonar  35460  goalrlem  35461  goalr  35462  fmla0disjsuc  35463  fmlasucdisj  35464  satffunlem1lem1  35467  satffunlem1lem2  35468  satffunlem2lem1  35469  mrsub0  35581  mrsubcn  35584  msubrn  35594  msubvrs  35625  br8  35821  br6  35822  br4  35823  cgrtriv  36067  btwntriv2  36077  btwncomim  36078  btwnswapid  36082  btwnintr  36084  btwnexch3  36085  btwnouttr2  36087  ifscgr  36109  cgrxfr  36120  btwnxfr  36121  btwnconn3  36168  segcon2  36170  brsegle  36173  seglecgr12im  36175  broutsideof3  36191  linethru  36218  elhf2  36240  opnregcld  36395  cldregopn  36396  neibastop2lem  36425  matunitlindflem1  37677  poimirlem16  37697  poimirlem17  37698  poimirlem19  37700  poimirlem20  37701  poimirlem24  37705  poimirlem29  37710  heicant  37716  opnmbllem0  37717  ismblfin  37722  itg2addnclem  37732  itg2addnclem3  37734  itg2gt0cn  37736  ftc1anclem5  37758  ftc2nc  37763  filbcmb  37801  fdc  37806  incsequz  37809  caushft  37822  istotbnd3  37832  equivbnd  37851  cntotbnd  37857  heibor1lem  37870  heibor1  37871  bfplem2  37884  divrngidl  38089  prnc  38128  lshpdisj  39107  cvrcon3b  39397  atnle  39437  hlhgt2  39509  hl0lt1N  39510  hl2at  39525  cvrexchlem  39539  cvratlem  39541  lvolnlelpln  39705  2lplnj  39740  ispsubcl2N  40067  lautcvr  40212  dva1dim  41105  dib1dim  41285  dib1dim2  41288  diclspsn  41314  dih1dimatlem  41449  dihlatat  41457  dihatexv  41458  dihatexv2  41459  lcfrlem9  41670  lcfrlem16  41678  mapdrvallem2  41765  mapd1o  41768  aks6d1c2  42244  elre0re  42373  prjspner1  42745  dffltz  42753  rexlimdv3d  42801  elrfi  42812  isnacs3  42828  eldiophb  42875  eldiophss  42892  diophren  42931  rencldnfilem  42938  pell1234qrdich  42979  pellfundex  43004  lsmfgcl  43192  kercvrlsm  43201  lmhmfgima  43202  lpirlnr  43235  hbtlem2  43242  hbtlem4  43244  hbtlem6  43247  rngunsnply  43287  onexoegt  43362  oaabsb  43412  cantnfresb  43442  omabs2  43450  tfsconcatrev  43466  restuni3  45240  limsupubuz  45836  stoweidlem57  46180  fourierdlem48  46277  fourierdlem49  46278  sge0le  46530  fsetsniunop  47174  cfsetsnfsetfo  47185  fcoresf1  47194  euoreqb  47234  modlt0b  47488  imasetpreimafvbijlemf1  47529  imasetpreimafvbijlemfo  47530  iccpartrn  47555  iccpartiun  47559  iccpartnel  47563  paireqne  47636  reupr  47647  odz2prm2pw  47688  fmtnofac2lem  47693  prmdvdsfmtnof1lem2  47710  2pwp1prm  47714  mod42tp1mod8  47727  lighneallem3  47732  lighneallem4  47735  requad01  47746  requad2  47748  fppr2odd  47856  gbowpos  47884  gbowgt5  47887  gboge9  47889  nnsum4primesodd  47921  nnsum4primesoddALTV  47922  isubgredg  47991  grimcnv  48013  uhgrimedgi  48015  isuspgrim0  48019  isuspgrimlem  48020  gricushgr  48042  clnbgrgrimlem  48058  clnbgrgrim  48059  grimedg  48060  grtrissvtx  48069  stgrusgra  48084  isubgr3stgrlem7  48097  gpgiedgdmellem  48171  gpgusgralem  48181  gpgvtxedg0  48188  gpgvtxedg1  48189  copisnmnd  48294  lidldomn1  48356  affinecomb1  48828  eenglngeehlnmlem2  48864  rrx2vlinest  48867  itsclquadb  48902  aacllem  49927