Theorem rexlimdva 3141

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-rex 3065

This theorem is referenced by:  rexlimdvaa  3142  rexlimivv  3182  rexlimdvv  3196  rspceb2dv  3571  ssexnelpss  4054  ralxfrd2  5348  iunopeqop  5469  iunopeqopOLD  5470  elsnxp  6249  foco2  7057  elunirn  7202  f1elima  7214  mptcnfimad  7935  releldmdifi  7994  mpoexw  8027  xpord3pred  8099  sexp3  8100  tfrlem9a  8322  seqomlem2  8387  oawordexr  8488  odi  8511  oelimcl  8533  nnawordex  8570  nnaordex  8571  oaabs  8581  oaabs2  8582  omabs  8584  eldifsucnn  8597  coflton  8604  cofon1  8605  cofon2  8606  cofonr  8607  naddunif  8626  ectocld  8726  onfin  9146  dif1ennnALT  9184  isfinite2  9205  isfiniteg  9207  fofinf1o  9239  elfiun  9340  suplub2  9371  supisoex  9385  ordtypelem9  9438  ordtypelem10  9439  brwdom2  9485  brwdom3  9494  ttrcltr  9635  rankr1ai  9720  fodomfi2  9980  infpwfien  9982  dfac12r  10067  ackbij1  10157  cff1  10178  fin23lem21  10259  isf32lem2  10274  fin1a2lem11  10330  fin1a2lem13  10332  ficard  10485  gchina  10620  eltsk2g  10672  tskr1om2  10689  rankcf  10698  inatsk  10699  tskuni  10704  nqereu  10850  ltexnq  10896  1idpr  10950  suplem1pr  10973  supsrlem  11032  axpre-sup  11090  1re  11142  0re  11144  0cnALT  11379  supaddc  12121  supadd  12122  supmul1  12123  supmul  12126  suprzcl2  12886  qmulz  12899  elpq  12923  qbtwnre  13149  ioo0  13321  ico0  13342  ioc0  13343  icc0  13344  addmodlteq  13906  fsequb  13935  hashdom  14339  ccats1alpha  14580  reuccatpfxs1lem  14706  shftlem  15028  rexuzre  15313  rexico  15314  caubnd  15319  limsupbnd1  15442  limsupbnd2  15443  rlim2lt  15457  rlim3  15458  lo1bdd2  15484  lo1bddrp  15485  o1lo1  15497  climuni  15512  climshftlem  15534  o1co  15546  rlimcn1  15548  climcn1  15552  o1rlimmul  15579  lo1le  15612  rlimno1  15614  isercoll  15628  caurcvg2  15638  serf0  15641  summolem2  15676  zsum  15678  fsum2dlem  15730  geomulcvg  15839  mertenslem2  15848  ntrivcvg  15860  zprod  15900  fprod2dlem  15943  dvds1lem  16234  dvdsexp2im  16294  odd2np1lem  16307  sqoddm1div8z  16321  ltoddhalfle  16328  halfleoddlt  16329  flodddiv4  16382  dvdssqim  16521  dvdsexpim  16522  coprmdvds2  16621  divgcdcoprm0  16632  cncongr1  16634  cncongr2  16635  isprm5  16675  rpexp  16690  pythagtriplem1  16785  iserodd  16804  pc2dvds  16848  difsqpwdvds  16856  oddprmdvds  16872  prmpwdvds  16873  4sqlem11  16924  vdwapun  16943  vdwlem2  16951  vdwlem6  16955  vdwlem8  16957  vdwlem10  16959  vdwnnlem1  16964  vdwnnlem3  16966  0ram  16989  ramub1lem2  16996  ramcl  16998  cshwsiun  17068  cshwrepswhash1  17071  firest  17393  imasvscafn  17499  imasmnd2  18740  dfgrp3lem  19012  imasgrp2  19029  issubg4  19119  cycsubm  19175  gaorber  19281  orbsta  19286  pmtr3ncom  19448  psgnran  19488  odmulg  19529  odbezout  19531  gexdvdsi  19556  sylow1lem3  19573  odcau  19577  sylow2alem1  19590  sylow3lem6  19605  lsmelvalm  19624  efgrelexlemb  19723  efgredeu  19725  imasabl  19849  cyggeninv  19856  cygctb  19865  cyggexb  19872  dprdssv  19991  dprddisj2  20014  ablfacrplem  20040  pgpfac1lem2  20050  pgpfac1lem5  20054  ringinvnzdiv  20280  imasring  20308  dvdsrcl2  20344  dvdsrmul1  20347  lss1d  20960  lssats2  20997  lspsn  20999  lmhmima  21044  ring2idlqusb  21310  rngqiprngfulem2  21312  lpiss  21329  dvdsrzring  21443  pzriprnglem5  21467  pzriprnglem8  21470  pzriprnglem10  21472  pzriprnglem11  21473  znunit  21545  znrrg  21547  cygznlem3  21551  frgpcyg  21555  lindfrn  21803  mplcoe5lem  22022  mpfind  22098  gsummoncoe1  22301  mpfpf1  22344  pf1mpf  22345  mat1dimelbas  22461  scmatdmat  22505  scmataddcl  22506  scmatsubcl  22507  scmatmulcl  22508  cpmatacl  22706  chpscmat  22832  tgcl  22959  clsval2  23040  innei  23115  restcld  23162  restcldr  23164  ordtrest2lem  23193  cnprest  23279  lmss  23288  lmcls  23292  lmcnp  23294  isreg2  23367  cmpcovf  23381  cncmp  23382  cmpsub  23390  1stcrest  23443  2ndcrest  23444  1stccnp  23452  restnlly  23472  cldllycmp  23485  locfincmp  23516  txcnpi  23598  pthaus  23628  txtube  23630  txcmplem1  23631  txcmplem2  23632  txlm  23638  xkohaus  23643  xkococnlem  23649  xkococn  23650  kqfvima  23720  kqreglem1  23731  isfild  23848  filuni  23875  isufil2  23898  uffix  23911  rnelfm  23943  fmfnfmlem2  23945  fmfnfmlem4  23947  fmfnfm  23948  fmco  23951  fclsopn  24004  ufilcmp  24022  cnpfcf  24031  alexsublem  24034  alexsubALT  24041  cldsubg  24101  ghmcnp  24105  qustgpopn  24110  tsmsgsum  24129  tsmsres  24134  tsmsxplem1  24143  tsmsxp  24145  isucn2  24268  ucnprima  24271  imasdsf1olem  24363  blssps  24414  blss  24415  blssexps  24416  blssex  24417  mopni3  24484  blcld  24495  metrest  24514  metcnp3  24530  reperflem  24809  icccmplem3  24815  xrge0tsms  24825  mulc1cncf  24897  cncfco  24899  cnheibor  24947  bndth  24950  lebnumlem3  24955  xlebnum  24957  lebnumii  24958  nmhmcn  25112  cfil3i  25261  cmetcaulem  25280  cfilres  25288  bcthlem4  25319  ivthlem2  25444  ivthlem3  25445  ivthicc  25450  cniccbdd  25453  ovolunlem1  25489  ovoliunlem2  25495  ovolshftlem2  25502  ovolicc2  25514  iunmbl2  25549  dyadmax  25590  opnmbllem  25593  subopnmbl  25596  volivth  25599  ismbf3d  25646  mbfimaopn2  25649  mbfaddlem  25652  i1fmullem  25686  mbfi1fseqlem4  25710  bddiblnc  25834  ellimc3  25871  dvlip  25985  dvlip2  25987  c1liplem1  25988  dvgt0lem1  25994  dvivthlem2  26001  dvne0  26003  lhop1lem  26005  lhop2  26007  lhop  26008  tdeglem4  26050  mdegnn0cl  26061  ply1divex  26127  dvdsq1p  26153  ig1peu  26165  elply2  26186  plypf1  26202  plydivex  26288  aalioulem3  26325  aalioulem5  26327  aaliou  26329  ulmshftlem  26379  ulmcau  26385  ulmss  26387  ulmbdd  26388  ulmcn  26389  radcnvlt1  26408  eflogeq  26591  efopn  26647  cxpeq  26746  angpieqvd  26820  xrlimcnp  26957  cxploglim  26966  ftalem2  27062  ftalem7  27067  isppw2  27103  dchrptlem1  27252  dchrptlem3  27254  dchrsum2  27256  lgsdchrval  27342  lgsdchr  27343  gausslemma2dlem1a  27353  lgsquadlem1  27368  2lgsoddprmlem2  27397  dchrisumlem3  27479  dchrisum0fno1  27499  pntlem3  27597  pntleml  27599  ostth3  27626  nosupno  27692  nosupbday  27694  noinfbday  27709  cutsun12  27807  oldssmade  27884  addsproplem2  27987  addsuniflem  28018  addbdaylem  28034  negsid  28058  negsunif  28072  negleft  28075  negright  28076  precsexlem6  28229  precsexlem7  28230  precsexlem11  28234  bdayons  28293  onaddscl  28294  om2noseqlt  28316  noseqrdgfn  28323  n0fincut  28372  bdayn0sf1o  28387  dfnns2  28389  bdaypw2n0bndlem  28480  bdayfinbndlem1  28484  z12negscl  28495  z12zsodd  28499  z12bdaylem  28501  bdayfinlem  28503  recut  28511  elreno2  28512  brcgr  28994  brbtwn2  28999  axbtwnid  29033  axcontlem7  29064  usgrnloopALT  29297  uhgrspansubgrlem  29384  nbuhgr  29437  nbupgr  29438  wwlksnextprop  30005  elwspths2on  30055  elwspths2onw  30056  erclwwlktr  30117  clwwlknscsh  30157  erclwwlkntr  30166  hashecclwwlkn1  30172  umgrhashecclwwlk  30173  3cyclfrgrrn1  30380  frgrregorufr  30420  frgr2wwlk1  30424  ubthlem1  30966  ubthlem3  30968  htthlem  31013  omlsii  31499  spansncol  31664  nmopun  32110  nmcexi  32122  riesz1  32161  elpjrn  32286  cvcon3  32380  chcv1  32451  atcvatlem  32481  chirredi  32490  br8d  32707  xrge0tsmsd  33161  ordtrest2NEWlem  34113  lmxrge0  34143  esumfsup  34261  esumpcvgval  34269  measdivcstALTV  34416  eulerpartlemgh  34569  dstfrvunirn  34666  afsval  34862  onvf1odlem4  35341  erdszelem8  35433  erdszelem11  35436  erdsze2lem2  35439  connpconn  35470  sconnpi1  35474  cvmsss2  35509  cvmfolem  35514  cvmliftmolem2  35517  cvmliftlem15  35533  cvmlift2lem1  35537  cvmlift3lem4  35557  cvmlift3lem5  35558  satfdmlem  35603  fmla1  35622  gonarlem  35629  gonar  35630  goalrlem  35631  goalr  35632  fmla0disjsuc  35633  fmlasucdisj  35634  satffunlem1lem1  35637  satffunlem1lem2  35638  satffunlem2lem1  35639  mrsub0  35751  mrsubcn  35754  msubrn  35764  msubvrs  35795  br8  35991  br6  35992  br4  35993  cgrtriv  36237  btwntriv2  36247  btwncomim  36248  btwnswapid  36252  btwnintr  36254  btwnexch3  36255  btwnouttr2  36257  ifscgr  36279  cgrxfr  36290  btwnxfr  36291  btwnconn3  36338  segcon2  36340  brsegle  36343  seglecgr12im  36345  broutsideof3  36361  linethru  36388  elhf2  36410  opnregcld  36565  cldregopn  36566  neibastop2lem  36595  tr0elw  36719  tr0el  36720  matunitlindflem1  37990  poimirlem16  38010  poimirlem17  38011  poimirlem19  38013  poimirlem20  38014  poimirlem24  38018  poimirlem29  38023  heicant  38029  opnmbllem0  38030  ismblfin  38035  itg2addnclem  38045  itg2addnclem3  38047  itg2gt0cn  38049  ftc1anclem5  38071  ftc2nc  38076  filbcmb  38114  fdc  38119  incsequz  38122  caushft  38135  istotbnd3  38145  equivbnd  38164  cntotbnd  38170  heibor1lem  38183  heibor1  38184  bfplem2  38197  divrngidl  38402  prnc  38441  lshpdisj  39486  cvrcon3b  39776  atnle  39816  hlhgt2  39888  hl0lt1N  39889  hl2at  39904  cvrexchlem  39918  cvratlem  39920  lvolnlelpln  40084  2lplnj  40119  ispsubcl2N  40446  lautcvr  40591  dva1dim  41484  dib1dim  41664  dib1dim2  41667  diclspsn  41693  dih1dimatlem  41828  dihlatat  41836  dihatexv  41837  dihatexv2  41838  lcfrlem9  42049  lcfrlem16  42057  mapdrvallem2  42144  mapd1o  42147  aks6d1c2  42622  elre0re  42745  prjspner1  43083  dffltz  43091  rexlimdv3d  43139  elrfi  43150  isnacs3  43166  eldiophb  43213  eldiophss  43230  diophren  43265  rencldnfilem  43272  pell1234qrdich  43313  pellfundex  43338  lsmfgcl  43526  kercvrlsm  43535  lmhmfgima  43536  lpirlnr  43569  hbtlem2  43576  hbtlem4  43578  hbtlem6  43581  rngunsnply  43621  onexoegt  43696  oaabsb  43746  cantnfresb  43776  omabs2  43784  tfsconcatrev  43800  restuni3  45572  limsupubuz  46163  stoweidlem57  46507  fourierdlem48  46604  fourierdlem49  46605  sge0le  46857  fsetsniunop  47519  cfsetsnfsetfo  47530  fcoresf1  47539  euoreqb  47579  modlt0b  47839  nndivides2  47854  imasetpreimafvbijlemf1  47886  imasetpreimafvbijlemfo  47887  iccpartrn  47912  iccpartiun  47916  iccpartnel  47920  paireqne  47993  reupr  48004  odz2prm2pw  48048  fmtnofac2lem  48053  prmdvdsfmtnof1lem2  48070  2pwp1prm  48074  mod42tp1mod8  48087  lighneallem3  48092  lighneallem4  48095  nprmdvdsfacm1  48109  ppivalnnprm  48110  ppivalnnnprmge6  48111  requad01  48119  requad2  48121  fppr2odd  48229  gbowpos  48257  gbowgt5  48260  gboge9  48262  nnsum4primesodd  48294  nnsum4primesoddALTV  48295  isubgredg  48364  grimcnv  48386  uhgrimedgi  48388  isuspgrim0  48392  isuspgrimlem  48393  gricushgr  48415  clnbgrgrimlem  48431  clnbgrgrim  48432  grimedg  48433  grtrissvtx  48442  stgrusgra  48457  isubgr3stgrlem7  48470  gpgiedgdmellem  48544  gpgusgralem  48554  gpgvtxedg0  48561  gpgvtxedg1  48562  copisnmnd  48667  lidldomn1  48729  affinecomb1  49200  eenglngeehlnmlem2  49236  rrx2vlinest  49239  itsclquadb  49274  aacllem  50298