Theorem rexlimdva 3161

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-rex 3077

This theorem is referenced by:  rexlimdvaa  3162  rexlimivv  3207  rexlimdvv  3218  rspceb2dv  3639  ssexnelpss  4139  ralxfrd2  5430  iunopeqop  5540  elsnxp  6322  foco2  7143  elunirn  7288  f1elima  7300  mptcnfimad  8027  releldmdifi  8086  mpoexw  8119  xpord3pred  8193  sexp3  8194  tfrlem9a  8442  seqomlem2  8507  oawordexr  8612  odi  8635  oelimcl  8656  nnawordex  8693  nnaordex  8694  oaabs  8704  oaabs2  8705  omabs  8707  eldifsucnn  8720  coflton  8727  cofon1  8728  cofon2  8729  cofonr  8730  naddunif  8749  ectocld  8842  onfin  9293  dif1ennnALT  9339  isfinite2  9362  isfiniteg  9365  fofinf1o  9400  elfiun  9499  suplub2  9530  supisoex  9543  ordtypelem9  9595  ordtypelem10  9596  brwdom2  9642  brwdom3  9651  ttrcltr  9785  rankr1ai  9867  fodomfi2  10129  infpwfien  10131  dfac12r  10216  ackbij1  10306  cff1  10327  fin23lem21  10408  isf32lem2  10423  fin1a2lem11  10479  fin1a2lem13  10481  ficard  10634  gchina  10768  eltsk2g  10820  tskr1om2  10837  rankcf  10846  inatsk  10847  tskuni  10852  nqereu  10998  ltexnq  11044  1idpr  11098  suplem1pr  11121  supsrlem  11180  axpre-sup  11238  1re  11290  0re  11292  0cnALT  11524  supaddc  12262  supadd  12263  supmul1  12264  supmul  12267  suprzcl2  13003  qmulz  13016  elpq  13040  qbtwnre  13261  ioo0  13432  ico0  13453  ioc0  13454  icc0  13455  addmodlteq  13997  fsequb  14026  hashdom  14428  ccats1alpha  14667  reuccatpfxs1lem  14794  shftlem  15117  rexuzre  15401  rexico  15402  caubnd  15407  limsupbnd1  15528  limsupbnd2  15529  rlim2lt  15543  rlim3  15544  lo1bdd2  15570  lo1bddrp  15571  o1lo1  15583  climuni  15598  climshftlem  15620  o1co  15632  rlimcn1  15634  climcn1  15638  o1rlimmul  15665  lo1le  15700  rlimno1  15702  isercoll  15716  caurcvg2  15726  serf0  15729  summolem2  15764  zsum  15766  fsum2dlem  15818  geomulcvg  15924  mertenslem2  15933  ntrivcvg  15945  zprod  15985  fprod2dlem  16028  dvds1lem  16316  dvdsexp2im  16375  odd2np1lem  16388  sqoddm1div8z  16402  ltoddhalfle  16409  halfleoddlt  16410  flodddiv4  16461  dvdssqim  16601  dvdsexpim  16602  coprmdvds2  16701  divgcdcoprm0  16712  cncongr1  16714  cncongr2  16715  isprm5  16754  rpexp  16769  pythagtriplem1  16863  iserodd  16882  pc2dvds  16926  difsqpwdvds  16934  oddprmdvds  16950  prmpwdvds  16951  4sqlem11  17002  vdwapun  17021  vdwlem2  17029  vdwlem6  17033  vdwlem8  17035  vdwlem10  17037  vdwnnlem1  17042  vdwnnlem3  17044  0ram  17067  ramub1lem2  17074  ramcl  17076  cshwsiun  17147  cshwrepswhash1  17150  firest  17492  imasvscafn  17597  imasmnd2  18809  dfgrp3lem  19078  imasgrp2  19095  issubg4  19185  cycsubm  19242  gaorber  19348  orbsta  19353  pmtr3ncom  19517  psgnran  19557  odmulg  19598  odbezout  19600  gexdvdsi  19625  sylow1lem3  19642  odcau  19646  sylow2alem1  19659  sylow3lem6  19674  lsmelvalm  19693  efgrelexlemb  19792  efgredeu  19794  imasabl  19918  cyggeninv  19925  cygctb  19934  cyggexb  19941  dprdssv  20060  dprddisj2  20083  ablfacrplem  20109  pgpfac1lem2  20119  pgpfac1lem5  20123  ringinvnzdiv  20324  imasring  20353  dvdsrcl2  20392  dvdsrmul1  20395  lss1d  20984  lssats2  21021  lspsn  21023  lmhmima  21069  ring2idlqusb  21343  rngqiprngfulem2  21345  lpiss  21362  dvdsrzring  21495  pzriprnglem5  21519  pzriprnglem8  21522  pzriprnglem10  21524  pzriprnglem11  21525  znunit  21605  znrrg  21607  cygznlem3  21611  frgpcyg  21615  lindfrn  21864  mplcoe5lem  22080  mpfind  22154  gsummoncoe1  22333  mpfpf1  22376  pf1mpf  22377  mat1dimelbas  22498  scmatdmat  22542  scmataddcl  22543  scmatsubcl  22544  scmatmulcl  22545  cpmatacl  22743  chpscmat  22869  tgcl  22997  clsval2  23079  innei  23154  restcld  23201  restcldr  23203  ordtrest2lem  23232  cnprest  23318  lmss  23327  lmcls  23331  lmcnp  23333  isreg2  23406  cmpcovf  23420  cncmp  23421  cmpsub  23429  1stcrest  23482  2ndcrest  23483  1stccnp  23491  restnlly  23511  cldllycmp  23524  locfincmp  23555  txcnpi  23637  pthaus  23667  txtube  23669  txcmplem1  23670  txcmplem2  23671  txlm  23677  xkohaus  23682  xkococnlem  23688  xkococn  23689  kqfvima  23759  kqreglem1  23770  isfild  23887  filuni  23914  isufil2  23937  uffix  23950  rnelfm  23982  fmfnfmlem2  23984  fmfnfmlem4  23986  fmfnfm  23987  fmco  23990  fclsopn  24043  ufilcmp  24061  cnpfcf  24070  alexsublem  24073  alexsubALT  24080  cldsubg  24140  ghmcnp  24144  qustgpopn  24149  tsmsgsum  24168  tsmsres  24173  tsmsxplem1  24182  tsmsxp  24184  isucn2  24309  ucnprima  24312  imasdsf1olem  24404  blssps  24455  blss  24456  blssexps  24457  blssex  24458  mopni3  24528  blcld  24539  metrest  24558  metcnp3  24574  reperflem  24859  icccmplem3  24865  xrge0tsms  24875  mulc1cncf  24950  cncfco  24952  cnheibor  25006  bndth  25009  lebnumlem3  25014  xlebnum  25016  lebnumii  25017  nmhmcn  25172  cfil3i  25322  cmetcaulem  25341  cfilres  25349  bcthlem4  25380  ivthlem2  25506  ivthlem3  25507  ivthicc  25512  cniccbdd  25515  ovolunlem1  25551  ovoliunlem2  25557  ovolshftlem2  25564  ovolicc2  25576  iunmbl2  25611  dyadmax  25652  opnmbllem  25655  subopnmbl  25658  volivth  25661  ismbf3d  25708  mbfimaopn2  25711  mbfaddlem  25714  i1fmullem  25748  mbfi1fseqlem4  25773  bddiblnc  25897  ellimc3  25934  dvlip  26052  dvlip2  26054  c1liplem1  26055  dvgt0lem1  26061  dvivthlem2  26068  dvne0  26070  lhop1lem  26072  lhop2  26074  lhop  26075  tdeglem4  26119  mdegnn0cl  26130  ply1divex  26196  dvdsq1p  26222  ig1peu  26234  elply2  26255  plypf1  26271  plydivex  26357  aalioulem3  26394  aalioulem5  26396  aaliou  26398  ulmshftlem  26450  ulmcau  26456  ulmss  26458  ulmbdd  26459  ulmcn  26460  radcnvlt1  26479  eflogeq  26662  efopn  26718  cxpeq  26818  angpieqvd  26892  xrlimcnp  27029  cxploglim  27039  ftalem2  27135  ftalem7  27140  isppw2  27176  dchrptlem1  27326  dchrptlem3  27328  dchrsum2  27330  lgsdchrval  27416  lgsdchr  27417  gausslemma2dlem1a  27427  lgsquadlem1  27442  2lgsoddprmlem2  27471  dchrisumlem3  27553  dchrisum0fno1  27573  pntlem3  27671  pntleml  27673  ostth3  27700  nosupno  27766  nosupbday  27768  noinfbday  27783  scutun12  27873  oldssmade  27934  addsproplem2  28021  addsuniflem  28052  addsbdaylem  28067  negsid  28091  negsunif  28105  precsexlem6  28254  precsexlem7  28255  precsexlem11  28259  onaddscl  28304  om2noseqlt  28323  noseqrdgfn  28330  dfnns2  28380  zs12bday  28442  recut  28446  brcgr  28933  brbtwn2  28938  axbtwnid  28972  axcontlem7  29003  usgrnloopALT  29238  uhgrspansubgrlem  29325  nbuhgr  29378  nbupgr  29379  wwlksnextprop  29945  elwspths2on  29993  erclwwlktr  30054  clwwlknscsh  30094  erclwwlkntr  30103  hashecclwwlkn1  30109  umgrhashecclwwlk  30110  3cyclfrgrrn1  30317  frgrregorufr  30357  frgr2wwlk1  30361  ubthlem1  30902  ubthlem3  30904  htthlem  30949  omlsii  31435  spansncol  31600  nmopun  32046  nmcexi  32058  riesz1  32097  elpjrn  32222  cvcon3  32316  chcv1  32387  atcvatlem  32417  chirredi  32426  br8d  32632  xrge0tsmsd  33041  ordtrest2NEWlem  33868  lmxrge0  33898  esumfsup  34034  esumpcvgval  34042  measdivcstALTV  34189  eulerpartlemgh  34343  dstfrvunirn  34439  afsval  34648  erdszelem8  35166  erdszelem11  35169  erdsze2lem2  35172  connpconn  35203  sconnpi1  35207  cvmsss2  35242  cvmfolem  35247  cvmliftmolem2  35250  cvmliftlem15  35266  cvmlift2lem1  35270  cvmlift3lem4  35290  cvmlift3lem5  35291  satfdmlem  35336  fmla1  35355  gonarlem  35362  gonar  35363  goalrlem  35364  goalr  35365  fmla0disjsuc  35366  fmlasucdisj  35367  satffunlem1lem1  35370  satffunlem1lem2  35371  satffunlem2lem1  35372  mrsub0  35484  mrsubcn  35487  msubrn  35497  msubvrs  35528  br8  35718  br6  35719  br4  35720  cgrtriv  35966  btwntriv2  35976  btwncomim  35977  btwnswapid  35981  btwnintr  35983  btwnexch3  35984  btwnouttr2  35986  ifscgr  36008  cgrxfr  36019  btwnxfr  36020  btwnconn3  36067  segcon2  36069  brsegle  36072  seglecgr12im  36074  broutsideof3  36090  linethru  36117  elhf2  36139  opnregcld  36296  cldregopn  36297  neibastop2lem  36326  matunitlindflem1  37576  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem24  37604  poimirlem29  37609  heicant  37615  opnmbllem0  37616  ismblfin  37621  itg2addnclem  37631  itg2addnclem3  37633  itg2gt0cn  37635  ftc1anclem5  37657  ftc2nc  37662  filbcmb  37700  fdc  37705  incsequz  37708  caushft  37721  istotbnd3  37731  equivbnd  37750  cntotbnd  37756  heibor1lem  37769  heibor1  37770  bfplem2  37783  divrngidl  37988  prnc  38027  lshpdisj  38943  cvrcon3b  39233  atnle  39273  hlhgt2  39346  hl0lt1N  39347  hl2at  39362  cvrexchlem  39376  cvratlem  39378  lvolnlelpln  39542  2lplnj  39577  ispsubcl2N  39904  lautcvr  40049  dva1dim  40942  dib1dim  41122  dib1dim2  41125  diclspsn  41151  dih1dimatlem  41286  dihlatat  41294  dihatexv  41295  dihatexv2  41296  lcfrlem9  41507  lcfrlem16  41515  mapdrvallem2  41602  mapd1o  41605  aks6d1c2  42087  elre0re  42249  prjspner1  42581  dffltz  42589  rexlimdv3d  42639  elrfi  42650  isnacs3  42666  eldiophb  42713  eldiophss  42730  diophren  42769  rencldnfilem  42776  pell1234qrdich  42817  pellfundex  42842  lsmfgcl  43031  kercvrlsm  43040  lmhmfgima  43041  lpirlnr  43074  hbtlem2  43081  hbtlem4  43083  hbtlem6  43086  rngunsnply  43130  onexoegt  43205  oaabsb  43256  cantnfresb  43286  omabs2  43294  tfsconcatrev  43310  restuni3  45020  limsupubuz  45634  stoweidlem57  45978  fourierdlem48  46075  fourierdlem49  46076  sge0le  46328  fsetsniunop  46964  cfsetsnfsetfo  46975  fcoresf1  46984  euoreqb  47024  imasetpreimafvbijlemf1  47278  imasetpreimafvbijlemfo  47279  iccpartrn  47304  iccpartiun  47308  iccpartnel  47312  paireqne  47385  reupr  47396  odz2prm2pw  47437  fmtnofac2lem  47442  prmdvdsfmtnof1lem2  47459  2pwp1prm  47463  mod42tp1mod8  47476  lighneallem3  47481  lighneallem4  47484  requad01  47495  requad2  47497  fppr2odd  47605  gbowpos  47633  gbowgt5  47636  gboge9  47638  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  isuspgrim0  47756  isuspgrimlem  47758  grimcnv  47763  gricushgr  47770  clnbgrgrimlem  47785  clnbgrgrim  47786  grimedg  47787  grtrissvtx  47795  copisnmnd  47892  lidldomn1  47954  affinecomb1  48436  eenglngeehlnmlem2  48472  rrx2vlinest  48475  itsclquadb  48510  aacllem  48895