Theorem rexlimdva 3137

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

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

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 3061

This theorem is referenced by:  rexlimdvaa  3138  rexlimivv  3178  rexlimdvv  3192  rspceb2dv  3580  ssexnelpss  4068  ralxfrd2  5357  iunopeqop  5469  elsnxp  6249  foco2  7054  elunirn  7197  f1elima  7209  mptcnfimad  7930  releldmdifi  7989  mpoexw  8022  xpord3pred  8094  sexp3  8095  tfrlem9a  8317  seqomlem2  8382  oawordexr  8483  odi  8506  oelimcl  8528  nnawordex  8565  nnaordex  8566  oaabs  8576  oaabs2  8577  omabs  8579  eldifsucnn  8592  coflton  8599  cofon1  8600  cofon2  8601  cofonr  8602  naddunif  8621  ectocld  8719  onfin  9139  dif1ennnALT  9177  isfinite2  9198  isfiniteg  9200  fofinf1o  9232  elfiun  9333  suplub2  9364  supisoex  9378  ordtypelem9  9431  ordtypelem10  9432  brwdom2  9478  brwdom3  9487  ttrcltr  9625  rankr1ai  9710  fodomfi2  9970  infpwfien  9972  dfac12r  10057  ackbij1  10147  cff1  10168  fin23lem21  10249  isf32lem2  10264  fin1a2lem11  10320  fin1a2lem13  10322  ficard  10475  gchina  10610  eltsk2g  10662  tskr1om2  10679  rankcf  10688  inatsk  10689  tskuni  10694  nqereu  10840  ltexnq  10886  1idpr  10940  suplem1pr  10963  supsrlem  11022  axpre-sup  11080  1re  11132  0re  11134  0cnALT  11368  supaddc  12109  supadd  12110  supmul1  12111  supmul  12114  suprzcl2  12851  qmulz  12864  elpq  12888  qbtwnre  13114  ioo0  13286  ico0  13307  ioc0  13308  icc0  13309  addmodlteq  13869  fsequb  13898  hashdom  14302  ccats1alpha  14543  reuccatpfxs1lem  14669  shftlem  14991  rexuzre  15276  rexico  15277  caubnd  15282  limsupbnd1  15405  limsupbnd2  15406  rlim2lt  15420  rlim3  15421  lo1bdd2  15447  lo1bddrp  15448  o1lo1  15460  climuni  15475  climshftlem  15497  o1co  15509  rlimcn1  15511  climcn1  15515  o1rlimmul  15542  lo1le  15575  rlimno1  15577  isercoll  15591  caurcvg2  15601  serf0  15604  summolem2  15639  zsum  15641  fsum2dlem  15693  geomulcvg  15799  mertenslem2  15808  ntrivcvg  15820  zprod  15860  fprod2dlem  15903  dvds1lem  16194  dvdsexp2im  16254  odd2np1lem  16267  sqoddm1div8z  16281  ltoddhalfle  16288  halfleoddlt  16289  flodddiv4  16342  dvdssqim  16481  dvdsexpim  16482  coprmdvds2  16581  divgcdcoprm0  16592  cncongr1  16594  cncongr2  16595  isprm5  16634  rpexp  16649  pythagtriplem1  16744  iserodd  16763  pc2dvds  16807  difsqpwdvds  16815  oddprmdvds  16831  prmpwdvds  16832  4sqlem11  16883  vdwapun  16902  vdwlem2  16910  vdwlem6  16914  vdwlem8  16916  vdwlem10  16918  vdwnnlem1  16923  vdwnnlem3  16925  0ram  16948  ramub1lem2  16955  ramcl  16957  cshwsiun  17027  cshwrepswhash1  17030  firest  17352  imasvscafn  17458  imasmnd2  18699  dfgrp3lem  18968  imasgrp2  18985  issubg4  19075  cycsubm  19131  gaorber  19237  orbsta  19242  pmtr3ncom  19404  psgnran  19444  odmulg  19485  odbezout  19487  gexdvdsi  19512  sylow1lem3  19529  odcau  19533  sylow2alem1  19546  sylow3lem6  19561  lsmelvalm  19580  efgrelexlemb  19679  efgredeu  19681  imasabl  19805  cyggeninv  19812  cygctb  19821  cyggexb  19828  dprdssv  19947  dprddisj2  19970  ablfacrplem  19996  pgpfac1lem2  20006  pgpfac1lem5  20010  ringinvnzdiv  20236  imasring  20266  dvdsrcl2  20302  dvdsrmul1  20305  lss1d  20914  lssats2  20951  lspsn  20953  lmhmima  20999  ring2idlqusb  21265  rngqiprngfulem2  21267  lpiss  21284  dvdsrzring  21416  pzriprnglem5  21440  pzriprnglem8  21443  pzriprnglem10  21445  pzriprnglem11  21446  znunit  21518  znrrg  21520  cygznlem3  21524  frgpcyg  21528  lindfrn  21776  mplcoe5lem  21994  mpfind  22070  gsummoncoe1  22252  mpfpf1  22295  pf1mpf  22296  mat1dimelbas  22415  scmatdmat  22459  scmataddcl  22460  scmatsubcl  22461  scmatmulcl  22462  cpmatacl  22660  chpscmat  22786  tgcl  22913  clsval2  22994  innei  23069  restcld  23116  restcldr  23118  ordtrest2lem  23147  cnprest  23233  lmss  23242  lmcls  23246  lmcnp  23248  isreg2  23321  cmpcovf  23335  cncmp  23336  cmpsub  23344  1stcrest  23397  2ndcrest  23398  1stccnp  23406  restnlly  23426  cldllycmp  23439  locfincmp  23470  txcnpi  23552  pthaus  23582  txtube  23584  txcmplem1  23585  txcmplem2  23586  txlm  23592  xkohaus  23597  xkococnlem  23603  xkococn  23604  kqfvima  23674  kqreglem1  23685  isfild  23802  filuni  23829  isufil2  23852  uffix  23865  rnelfm  23897  fmfnfmlem2  23899  fmfnfmlem4  23901  fmfnfm  23902  fmco  23905  fclsopn  23958  ufilcmp  23976  cnpfcf  23985  alexsublem  23988  alexsubALT  23995  cldsubg  24055  ghmcnp  24059  qustgpopn  24064  tsmsgsum  24083  tsmsres  24088  tsmsxplem1  24097  tsmsxp  24099  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  25225  cmetcaulem  25244  cfilres  25252  bcthlem4  25283  ivthlem2  25409  ivthlem3  25410  ivthicc  25415  cniccbdd  25418  ovolunlem1  25454  ovoliunlem2  25460  ovolshftlem2  25467  ovolicc2  25479  iunmbl2  25514  dyadmax  25555  opnmbllem  25558  subopnmbl  25561  volivth  25564  ismbf3d  25611  mbfimaopn2  25614  mbfaddlem  25617  i1fmullem  25651  mbfi1fseqlem4  25675  bddiblnc  25799  ellimc3  25836  dvlip  25954  dvlip2  25956  c1liplem1  25957  dvgt0lem1  25963  dvivthlem2  25970  dvne0  25972  lhop1lem  25974  lhop2  25976  lhop  25977  tdeglem4  26021  mdegnn0cl  26032  ply1divex  26098  dvdsq1p  26124  ig1peu  26136  elply2  26157  plypf1  26173  plydivex  26261  aalioulem3  26298  aalioulem5  26300  aaliou  26302  ulmshftlem  26354  ulmcau  26360  ulmss  26362  ulmbdd  26363  ulmcn  26364  radcnvlt1  26383  eflogeq  26567  efopn  26623  cxpeq  26723  angpieqvd  26797  xrlimcnp  26934  cxploglim  26944  ftalem2  27040  ftalem7  27045  isppw2  27081  dchrptlem1  27231  dchrptlem3  27233  dchrsum2  27235  lgsdchrval  27321  lgsdchr  27322  gausslemma2dlem1a  27332  lgsquadlem1  27347  2lgsoddprmlem2  27376  dchrisumlem3  27458  dchrisum0fno1  27478  pntlem3  27576  pntleml  27578  ostth3  27605  nosupno  27671  nosupbday  27673  noinfbday  27688  cutsun12  27786  oldssmade  27863  addsproplem2  27966  addsuniflem  27997  addbdaylem  28013  negsid  28037  negsunif  28051  negleft  28054  negright  28055  precsexlem6  28208  precsexlem7  28209  precsexlem11  28213  bdayons  28272  onaddscl  28273  om2noseqlt  28295  noseqrdgfn  28302  n0fincut  28351  bdayn0sf1o  28366  dfnns2  28368  bdaypw2n0bndlem  28459  bdayfinbndlem1  28463  z12negscl  28474  z12zsodd  28478  z12bdaylem  28480  bdayfinlem  28482  recut  28490  elreno2  28491  brcgr  28973  brbtwn2  28978  axbtwnid  29012  axcontlem7  29043  usgrnloopALT  29276  uhgrspansubgrlem  29363  nbuhgr  29416  nbupgr  29417  wwlksnextprop  29985  elwspths2on  30035  elwspths2onw  30036  erclwwlktr  30097  clwwlknscsh  30137  erclwwlkntr  30146  hashecclwwlkn1  30152  umgrhashecclwwlk  30153  3cyclfrgrrn1  30360  frgrregorufr  30400  frgr2wwlk1  30404  ubthlem1  30945  ubthlem3  30947  htthlem  30992  omlsii  31478  spansncol  31643  nmopun  32089  nmcexi  32101  riesz1  32140  elpjrn  32265  cvcon3  32359  chcv1  32430  atcvatlem  32460  chirredi  32469  br8d  32686  xrge0tsmsd  33155  ordtrest2NEWlem  34079  lmxrge0  34109  esumfsup  34227  esumpcvgval  34235  measdivcstALTV  34382  eulerpartlemgh  34535  dstfrvunirn  34632  afsval  34828  onvf1odlem4  35300  erdszelem8  35392  erdszelem11  35395  erdsze2lem2  35398  connpconn  35429  sconnpi1  35433  cvmsss2  35468  cvmfolem  35473  cvmliftmolem2  35476  cvmliftlem15  35492  cvmlift2lem1  35496  cvmlift3lem4  35516  cvmlift3lem5  35517  satfdmlem  35562  fmla1  35581  gonarlem  35588  gonar  35589  goalrlem  35590  goalr  35591  fmla0disjsuc  35592  fmlasucdisj  35593  satffunlem1lem1  35596  satffunlem1lem2  35597  satffunlem2lem1  35598  mrsub0  35710  mrsubcn  35713  msubrn  35723  msubvrs  35754  br8  35950  br6  35951  br4  35952  cgrtriv  36196  btwntriv2  36206  btwncomim  36207  btwnswapid  36211  btwnintr  36213  btwnexch3  36214  btwnouttr2  36216  ifscgr  36238  cgrxfr  36249  btwnxfr  36250  btwnconn3  36297  segcon2  36299  brsegle  36302  seglecgr12im  36304  broutsideof3  36320  linethru  36347  elhf2  36369  opnregcld  36524  cldregopn  36525  neibastop2lem  36554  matunitlindflem1  37817  poimirlem16  37837  poimirlem17  37838  poimirlem19  37840  poimirlem20  37841  poimirlem24  37845  poimirlem29  37850  heicant  37856  opnmbllem0  37857  ismblfin  37862  itg2addnclem  37872  itg2addnclem3  37874  itg2gt0cn  37876  ftc1anclem5  37898  ftc2nc  37903  filbcmb  37941  fdc  37946  incsequz  37949  caushft  37962  istotbnd3  37972  equivbnd  37991  cntotbnd  37997  heibor1lem  38010  heibor1  38011  bfplem2  38024  divrngidl  38229  prnc  38268  lshpdisj  39247  cvrcon3b  39537  atnle  39577  hlhgt2  39649  hl0lt1N  39650  hl2at  39665  cvrexchlem  39679  cvratlem  39681  lvolnlelpln  39845  2lplnj  39880  ispsubcl2N  40207  lautcvr  40352  dva1dim  41245  dib1dim  41425  dib1dim2  41428  diclspsn  41454  dih1dimatlem  41589  dihlatat  41597  dihatexv  41598  dihatexv2  41599  lcfrlem9  41810  lcfrlem16  41818  mapdrvallem2  41905  mapd1o  41908  aks6d1c2  42384  elre0re  42509  prjspner1  42869  dffltz  42877  rexlimdv3d  42925  elrfi  42936  isnacs3  42952  eldiophb  42999  eldiophss  43016  diophren  43055  rencldnfilem  43062  pell1234qrdich  43103  pellfundex  43128  lsmfgcl  43316  kercvrlsm  43325  lmhmfgima  43326  lpirlnr  43359  hbtlem2  43366  hbtlem4  43368  hbtlem6  43371  rngunsnply  43411  onexoegt  43486  oaabsb  43536  cantnfresb  43566  omabs2  43574  tfsconcatrev  43590  restuni3  45362  limsupubuz  45957  stoweidlem57  46301  fourierdlem48  46398  fourierdlem49  46399  sge0le  46651  fsetsniunop  47295  cfsetsnfsetfo  47306  fcoresf1  47315  euoreqb  47355  modlt0b  47609  imasetpreimafvbijlemf1  47650  imasetpreimafvbijlemfo  47651  iccpartrn  47676  iccpartiun  47680  iccpartnel  47684  paireqne  47757  reupr  47768  odz2prm2pw  47809  fmtnofac2lem  47814  prmdvdsfmtnof1lem2  47831  2pwp1prm  47835  mod42tp1mod8  47848  lighneallem3  47853  lighneallem4  47856  requad01  47867  requad2  47869  fppr2odd  47977  gbowpos  48005  gbowgt5  48008  gboge9  48010  nnsum4primesodd  48042  nnsum4primesoddALTV  48043  isubgredg  48112  grimcnv  48134  uhgrimedgi  48136  isuspgrim0  48140  isuspgrimlem  48141  gricushgr  48163  clnbgrgrimlem  48179  clnbgrgrim  48180  grimedg  48181  grtrissvtx  48190  stgrusgra  48205  isubgr3stgrlem7  48218  gpgiedgdmellem  48292  gpgusgralem  48302  gpgvtxedg0  48309  gpgvtxedg1  48310  copisnmnd  48415  lidldomn1  48477  affinecomb1  48948  eenglngeehlnmlem2  48984  rrx2vlinest  48987  itsclquadb  49022  aacllem  50046