Theorem rexlimdva 3166

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 417	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	rexlimdv 3164	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2145  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-rex 3090

This theorem is referenced by:  rexlimdvaa  3167  rexlimivv  3207  rexlimdvv  3221  rspceb2dv  3588  ssexnelpss  4073  ralxfrd2  5374  iunopeqop  5495  iunopeqopOLD  5496  elsnxp  6282  foco2  7094  elunirn  7239  f1elima  7251  mptcnfimad  7971  releldmdifi  8030  mpoexw  8063  xpord3pred  8136  sexp3  8137  tfrlem9a  8361  seqomlem2  8426  oawordexr  8529  odi  8552  oelimcl  8574  nnawordex  8611  nnaordex  8612  oaabs  8622  oaabs2  8623  omabs  8625  eldifsucnn  8638  coflton  8645  cofon1  8646  cofon2  8647  cofonr  8648  naddunif  8668  ectocld  8768  onfin  9187  dif1ennnALT  9225  isfinite2  9246  isfiniteg  9248  fofinf1o  9277  elfiun  9378  suplub2  9409  supisoex  9423  ordtypelem9  9476  ordtypelem10  9477  brwdom2  9523  brwdom3  9532  ttrcltr  9673  rankr1ai  9758  fodomfi2  10032  infpwfien  10034  dfac12r  10118  ackbij1  10208  cff1  10230  fin23lem21  10311  isf32lem2  10326  fin1a2lem11  10382  fin1a2lem13  10384  ficard  10537  gchina  10672  eltsk2g  10724  tskr1om2  10741  rankcf  10750  inatsk  10751  tskuni  10756  nqereu  10902  ltexnq  10948  1idpr  11002  suplem1pr  11025  supsrlem  11084  axpre-sup  11142  1re  11196  0re  11198  0cnALT  11433  supaddc  12173  supadd  12174  supmul1  12175  supmul  12178  suprzcl2  12953  qmulz  12966  elpq  12990  qbtwnre  13216  ioo0  13388  ico0  13409  ioc0  13410  icc0  13411  addmodlteq  13973  fsequb  14002  hashdom  14406  ccats1alpha  14647  reuccatpfxs1lem  14773  shftlem  15095  rexuzre  15394  rexico  15395  caubnd  15400  limsupbnd1  15523  limsupbnd2  15524  rlim2lt  15538  rlim3  15539  lo1bdd2  15565  lo1bddrp  15566  o1lo1  15578  climuni  15593  climshftlem  15615  o1co  15627  rlimcn1  15629  climcn1  15633  o1rlimmul  15660  lo1le  15693  rlimno1  15695  isercoll  15709  caurcvg2  15719  serf0  15722  summolem2  15757  zsum  15759  fsum2dlem  15811  geomulcvg  15920  mertenslem2  15929  ntrivcvg  15941  zprod  15981  fprod2dlem  16024  dvds1lem  16315  dvdsexp2im  16375  odd2np1lem  16388  sqoddm1div8z  16402  ltoddhalfle  16409  halfleoddlt  16410  flodddiv4  16463  dvdssqim  16602  dvdsexpim  16603  coprmdvds2  16702  divgcdcoprm0  16713  cncongr1  16715  cncongr2  16716  isprm5  16756  rpexp  16771  pythagtriplem1  16866  iserodd  16885  pc2dvds  16929  difsqpwdvds  16937  oddprmdvds  16953  prmpwdvds  16954  4sqlem11  17005  vdwapun  17024  vdwlem2  17032  vdwlem6  17036  vdwlem8  17038  vdwlem10  17040  vdwnnlem1  17045  vdwnnlem3  17047  0ram  17070  ramub1lem2  17077  ramcl  17079  cshwsiun  17149  cshwrepswhash1  17152  firest  17475  imasvscafn  17581  imasmnd2  18822  dfgrp3lem  19095  imasgrp2  19112  issubg4  19203  cycsubm  19264  gaorber  19369  orbsta  19374  pmtr3ncom  19536  psgnran  19576  odmulg  19617  odbezout  19619  gexdvdsi  19644  sylow1lem3  19661  odcau  19665  sylow2alem1  19678  sylow3lem6  19693  lsmelvalm  19712  efgrelexlemb  19811  efgredeu  19813  imasabl  19937  cyggeninv  19944  cygctb  19953  cyggexb  19960  dprdssv  20079  dprddisj2  20102  ablfacrplem  20128  pgpfac1lem2  20138  pgpfac1lem5  20142  ringinvnzdiv  20375  imasring  20403  dvdsrcl2  20439  dvdsrmul1  20442  lss1d  21053  lssats2  21090  lspsn  21092  lmhmima  21137  ring2idlqusb  21412  rngqiprngfulem2  21414  lpiss  21457  dvdsrzring  21571  pzriprnglem5  21595  pzriprnglem8  21598  pzriprnglem10  21600  pzriprnglem11  21601  znunit  21673  znrrg  21675  cygznlem3  21679  frgpcyg  21683  lindfrn  21931  mplcoe5lem  22150  mpfind  22226  gsummoncoe1  22429  mpfpf1  22472  pf1mpf  22473  mat1dimelbas  22589  scmatdmat  22633  scmataddcl  22634  scmatsubcl  22635  scmatmulcl  22636  cpmatacl  22834  chpscmat  22960  tgcl  23087  clsval2  23168  innei  23243  restcld  23290  restcldr  23292  ordtrest2lem  23321  cnprest  23407  lmss  23416  lmcls  23420  lmcnp  23422  isreg2  23495  cmpcovf  23509  cncmp  23510  cmpsub  23518  1stcrest  23571  2ndcrest  23572  1stccnp  23580  restnlly  23600  cldllycmp  23613  locfincmp  23644  txcnpi  23726  pthaus  23756  txtube  23758  txcmplem1  23759  txcmplem2  23760  txlm  23766  xkohaus  23771  xkococnlem  23777  xkococn  23778  kqfvima  23848  kqreglem1  23859  isfild  23976  filuni  24003  isufil2  24026  uffix  24039  rnelfm  24071  fmfnfmlem2  24073  fmfnfmlem4  24075  fmfnfm  24076  fmco  24079  fclsopn  24132  ufilcmp  24150  cnpfcf  24159  alexsublem  24162  alexsubALT  24169  cldsubg  24229  ghmcnp  24233  qustgpopn  24238  tsmsgsum  24257  tsmsres  24262  tsmsxplem1  24271  tsmsxp  24273  isucn2  24396  ucnprima  24399  imasdsf1olem  24491  blssps  24542  blss  24543  blssexps  24544  blssex  24545  mopni3  24612  blcld  24623  metrest  24642  metcnp3  24658  reperflem  24937  icccmplem3  24943  xrge0tsms  24953  mulc1cncf  25025  cncfco  25027  cnheibor  25075  bndth  25078  lebnumlem3  25083  xlebnum  25085  lebnumii  25086  nmhmcn  25240  cfil3i  25389  cmetcaulem  25408  cfilres  25416  bcthlem4  25447  ivthlem2  25572  ivthlem3  25573  ivthicc  25578  cniccbdd  25581  ovolunlem1  25617  ovoliunlem2  25623  ovolshftlem2  25630  ovolicc2  25642  iunmbl2  25677  dyadmax  25718  opnmbllem  25721  subopnmbl  25724  volivth  25727  ismbf3d  25774  mbfimaopn2  25777  mbfaddlem  25780  i1fmullem  25814  mbfi1fseqlem4  25838  bddiblnc  25962  ellimc3  25999  dvlip  26113  dvlip2  26115  c1liplem1  26116  dvgt0lem1  26122  dvivthlem2  26129  dvne0  26131  lhop1lem  26133  lhop2  26135  lhop  26136  tdeglem4  26178  mdegnn0cl  26189  ply1divex  26255  dvdsq1p  26281  ig1peu  26293  elply2  26314  plypf1  26330  plydivex  26419  aalioulem3  26456  aalioulem5  26458  aaliou  26460  ulmshftlem  26510  ulmcau  26516  ulmss  26518  ulmbdd  26519  ulmcn  26520  radcnvlt1  26539  eflogeq  26725  efopn  26781  cxpeq  26880  angpieqvd  26954  xrlimcnp  27091  cxploglim  27100  ftalem2  27196  ftalem7  27201  isppw2  27237  dchrptlem1  27386  dchrptlem3  27388  dchrsum2  27390  lgsdchrval  27476  lgsdchr  27477  gausslemma2dlem1a  27487  lgsquadlem1  27502  2lgsoddprmlem2  27531  dchrisumlem3  27613  dchrisum0fno1  27633  pntlem3  27731  pntleml  27733  ostth3  27760  nosupno  27825  nosupbday  27827  noinfbday  27842  cutsun12  27941  oldssmade  28018  addsproplem2  28121  addsuniflem  28152  addbdaylem  28168  negsid  28192  negsunif  28206  negleft  28209  negright  28210  precsexlem6  28363  precsexlem7  28364  precsexlem11  28368  bdayons  28427  onaddscl  28428  om2noseqlt  28450  noseqrdgfn  28457  n0fincut  28506  bdayn0sf1o  28521  dfnns2  28523  bdaypw2n0bndlem  28614  bdayfinbndlem1  28618  z12negscl  28629  z12zsodd  28633  z12bdaylem  28635  bdayfinlem  28637  recut  28645  elreno2  28646  brcgr  29159  brbtwn2  29164  axbtwnid  29198  axcontlem7  29229  usgrnloopALT  29462  uhgrspansubgrlem  29549  nbuhgr  29602  nbupgr  29603  wwlksnextprop  30170  elwspths2on  30220  elwspths2onw  30221  erclwwlktr  30282  clwwlknscsh  30322  erclwwlkntr  30331  hashecclwwlkn1  30337  umgrhashecclwwlk  30338  3cyclfrgrrn1  30545  frgrregorufr  30585  frgr2wwlk1  30589  ubthlem1  31131  ubthlem3  31133  htthlem  31178  omlsii  31664  spansncol  31829  nmopun  32275  nmcexi  32287  riesz1  32326  elpjrn  32451  cvcon3  32545  chcv1  32616  atcvatlem  32646  chirredi  32655  br8d  32865  xrge0tsmsd  33306  ordtrest2NEWlem  34229  lmxrge0  34259  esumfsup  34377  esumpcvgval  34385  measdivcstALTV  34532  eulerpartlemgh  34685  dstfrvunirn  34782  afsval  34978  onvf1odlem4  35461  erdszelem8  35561  erdszelem11  35564  erdsze2lem2  35567  connpconn  35598  sconnpi1  35602  cvmsss2  35637  cvmfolem  35642  cvmliftmolem2  35645  cvmliftlem15  35661  cvmlift2lem1  35665  cvmlift3lem4  35685  cvmlift3lem5  35686  satfdmlem  35731  fmla1  35750  gonarlem  35757  gonar  35758  goalrlem  35759  goalr  35760  fmla0disjsuc  35761  fmlasucdisj  35762  satffunlem1lem1  35765  satffunlem1lem2  35766  satffunlem2lem1  35767  mrsub0  35879  mrsubcn  35882  msubrn  35892  msubvrs  35923  br8  36119  br6  36120  br4  36121  cgrtriv  36365  btwntriv2  36375  btwncomim  36376  btwnswapid  36380  btwnintr  36382  btwnexch3  36383  btwnouttr2  36385  ifscgr  36407  cgrxfr  36418  btwnxfr  36419  btwnconn3  36466  segcon2  36468  brsegle  36471  seglecgr12im  36473  broutsideof3  36489  linethru  36516  elhf2  36538  nmulprop  36553  opnregcld  36703  cldregopn  36704  neibastop2lem  36733  tr0elw  36857  tr0el  36858  matunitlindflem1  38127  poimirlem16  38147  poimirlem17  38148  poimirlem19  38150  poimirlem20  38151  poimirlem24  38155  poimirlem29  38160  heicant  38166  opnmbllem0  38167  ismblfin  38172  itg2addnclem  38182  itg2addnclem3  38184  itg2gt0cn  38186  ftc1anclem5  38208  ftc2nc  38213  filbcmb  38251  fdc  38256  incsequz  38259  caushft  38272  istotbnd3  38282  equivbnd  38301  cntotbnd  38307  heibor1lem  38320  heibor1  38321  bfplem2  38334  divrngidl  38539  prnc  38578  lshpdisj  39623  cvrcon3b  39913  atnle  39953  hlhgt2  40025  hl0lt1N  40026  hl2at  40041  cvrexchlem  40055  cvratlem  40057  lvolnlelpln  40221  2lplnj  40256  ispsubcl2N  40583  lautcvr  40728  dva1dim  41621  dib1dim  41801  dib1dim2  41804  diclspsn  41830  dih1dimatlem  41965  dihlatat  41973  dihatexv  41974  dihatexv2  41975  lcfrlem9  42186  lcfrlem16  42194  mapdrvallem2  42281  mapd1o  42284  aks6d1c2  42759  elre0re  42882  prjspner1  43220  dffltz  43228  rexlimdv3d  43276  elrfi  43287  isnacs3  43303  eldiophb  43350  eldiophss  43367  diophren  43402  rencldnfilem  43409  pell1234qrdich  43450  pellfundex  43475  lsmfgcl  43663  kercvrlsm  43672  lmhmfgima  43673  lpirlnr  43706  hbtlem2  43713  hbtlem4  43715  hbtlem6  43718  rngunsnply  43758  onexoegt  43833  oaabsb  43883  cantnfresb  43913  omabs2  43921  tfsconcatrev  43937  restuni3  45694  limsupubuz  46285  stoweidlem57  46629  fourierdlem48  46726  fourierdlem49  46727  sge0le  46979  fsetsniunop  47641  cfsetsnfsetfo  47652  fcoresf1  47661  euoreqb  47701  modlt0b  47961  nndivides2  47976  imasetpreimafvbijlemf1  48008  imasetpreimafvbijlemfo  48009  iccpartrn  48034  iccpartiun  48038  iccpartnel  48042  paireqne  48115  reupr  48126  odz2prm2pw  48170  fmtnofac2lem  48175  prmdvdsfmtnof1lem2  48192  2pwp1prm  48196  mod42tp1mod8  48209  lighneallem3  48214  lighneallem4  48217  nprmdvdsfacm1  48231  ppivalnnprm  48232  ppivalnnnprmge6  48233  requad01  48241  requad2  48243  fppr2odd  48351  gbowpos  48379  gbowgt5  48382  gboge9  48384  nnsum4primesodd  48416  nnsum4primesoddALTV  48417  isubgredg  48486  grimcnv  48508  uhgrimedgi  48510  isuspgrim0  48514  isuspgrimlem  48515  gricushgr  48537  clnbgrgrimlem  48553  clnbgrgrim  48554  grimedg  48555  grtrissvtx  48564  stgrusgra  48579  isubgr3stgrlem7  48592  gpgiedgdmellem  48666  gpgusgralem  48676  gpgvtxedg0  48683  gpgvtxedg1  48684  copisnmnd  48789  lidldomn1  48851  affinecomb1  49333  eenglngeehlnmlem2  49369  rrx2vlinest  49372  itsclquadb  49407  aacllem  50430