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  37813  poimirlem16  37833  poimirlem17  37834  poimirlem19  37836  poimirlem20  37837  poimirlem24  37841  poimirlem29  37846  heicant  37852  opnmbllem0  37853  ismblfin  37858  itg2addnclem  37868  itg2addnclem3  37870  itg2gt0cn  37872  ftc1anclem5  37894  ftc2nc  37899  filbcmb  37937  fdc  37942  incsequz  37945  caushft  37958  istotbnd3  37968  equivbnd  37987  cntotbnd  37993  heibor1lem  38006  heibor1  38007  bfplem2  38020  divrngidl  38225  prnc  38264  lshpdisj  39243  cvrcon3b  39533  atnle  39573  hlhgt2  39645  hl0lt1N  39646  hl2at  39661  cvrexchlem  39675  cvratlem  39677  lvolnlelpln  39841  2lplnj  39876  ispsubcl2N  40203  lautcvr  40348  dva1dim  41241  dib1dim  41421  dib1dim2  41424  diclspsn  41450  dih1dimatlem  41585  dihlatat  41593  dihatexv  41594  dihatexv2  41595  lcfrlem9  41806  lcfrlem16  41814  mapdrvallem2  41901  mapd1o  41904  aks6d1c2  42380  elre0re  42505  prjspner1  42865  dffltz  42873  rexlimdv3d  42921  elrfi  42932  isnacs3  42948  eldiophb  42995  eldiophss  43012  diophren  43051  rencldnfilem  43058  pell1234qrdich  43099  pellfundex  43124  lsmfgcl  43312  kercvrlsm  43321  lmhmfgima  43322  lpirlnr  43355  hbtlem2  43362  hbtlem4  43364  hbtlem6  43367  rngunsnply  43407  onexoegt  43482  oaabsb  43532  cantnfresb  43562  omabs2  43570  tfsconcatrev  43586  restuni3  45358  limsupubuz  45953  stoweidlem57  46297  fourierdlem48  46394  fourierdlem49  46395  sge0le  46647  fsetsniunop  47291  cfsetsnfsetfo  47302  fcoresf1  47311  euoreqb  47351  modlt0b  47605  imasetpreimafvbijlemf1  47646  imasetpreimafvbijlemfo  47647  iccpartrn  47672  iccpartiun  47676  iccpartnel  47680  paireqne  47753  reupr  47764  odz2prm2pw  47805  fmtnofac2lem  47810  prmdvdsfmtnof1lem2  47827  2pwp1prm  47831  mod42tp1mod8  47844  lighneallem3  47849  lighneallem4  47852  requad01  47863  requad2  47865  fppr2odd  47973  gbowpos  48001  gbowgt5  48004  gboge9  48006  nnsum4primesodd  48038  nnsum4primesoddALTV  48039  isubgredg  48108  grimcnv  48130  uhgrimedgi  48132  isuspgrim0  48136  isuspgrimlem  48137  gricushgr  48159  clnbgrgrimlem  48175  clnbgrgrim  48176  grimedg  48177  grtrissvtx  48186  stgrusgra  48201  isubgr3stgrlem7  48214  gpgiedgdmellem  48288  gpgusgralem  48298  gpgvtxedg0  48305  gpgvtxedg1  48306  copisnmnd  48411  lidldomn1  48473  affinecomb1  48944  eenglngeehlnmlem2  48980  rrx2vlinest  48983  itsclquadb  49018  aacllem  50042