Theorem rexlimdva 3213

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∃wrex 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-ral 3069  df-rex 3070

This theorem is referenced by:  rexlimdvaa  3214  rexlimivv  3221  rexlimdvv  3222  ssexnelpss  4048  ralxfrd2  5335  iunopeqop  5435  elsnxp  6194  foco2  6983  elunirn  7124  f1elima  7136  releldmdifi  7886  mpoexw  7919  tfrlem9a  8217  seqomlem2  8282  oawordexr  8387  odi  8410  oelimcl  8431  nnawordex  8468  nnaordex  8469  oaabs  8478  oaabs2  8479  omabs  8481  eldifsucnn  8494  ectocld  8573  onfin  9013  dif1enALT  9050  isfinite2  9072  isfiniteg  9074  fofinf1o  9094  elfiun  9189  suplub2  9220  supisoex  9233  ordtypelem9  9285  ordtypelem10  9286  brwdom2  9332  brwdom3  9341  ttrcltr  9474  rankr1ai  9556  fodomfi2  9816  infpwfien  9818  dfac12r  9902  ackbij1  9994  cff1  10014  fin23lem21  10095  isf32lem2  10110  fin1a2lem11  10166  fin1a2lem13  10168  ficard  10321  gchina  10455  eltsk2g  10507  tskr1om2  10524  rankcf  10533  inatsk  10534  tskuni  10539  nqereu  10685  ltexnq  10731  1idpr  10785  suplem1pr  10808  supsrlem  10867  axpre-sup  10925  1re  10975  0re  10977  0cnALT  11209  negfi  11924  supaddc  11942  supadd  11943  supmul1  11944  supmul  11947  suprzcl2  12678  qmulz  12691  elpq  12715  qbtwnre  12933  ioo0  13104  ico0  13125  ioc0  13126  icc0  13127  addmodlteq  13666  fsequb  13695  hashdom  14094  ccats1alpha  14324  reuccatpfxs1lem  14459  shftlem  14779  rexuzre  15064  rexico  15065  caubnd  15070  limsupbnd1  15191  limsupbnd2  15192  rlim2lt  15206  rlim3  15207  lo1bdd2  15233  lo1bddrp  15234  o1lo1  15246  climuni  15261  climshftlem  15283  o1co  15295  rlimcn1  15297  climcn1  15301  o1rlimmul  15328  lo1le  15363  rlimno1  15365  isercoll  15379  caurcvg2  15389  serf0  15392  summolem2  15428  zsum  15430  fsum2dlem  15482  geomulcvg  15588  mertenslem2  15597  ntrivcvg  15609  zprod  15647  fprod2dlem  15690  dvds1lem  15977  dvdsexp2im  16036  odd2np1lem  16049  sqoddm1div8z  16063  ltoddhalfle  16070  halfleoddlt  16071  flodddiv4  16122  dvdssqim  16264  coprmdvds2  16359  divgcdcoprm0  16370  cncongr1  16372  cncongr2  16373  isprm5  16412  rpexp  16427  pythagtriplem1  16517  iserodd  16536  pc2dvds  16580  difsqpwdvds  16588  oddprmdvds  16604  prmpwdvds  16605  4sqlem11  16656  vdwapun  16675  vdwlem2  16683  vdwlem6  16687  vdwlem8  16689  vdwlem10  16691  vdwnnlem1  16696  vdwnnlem3  16698  0ram  16721  ramub1lem2  16728  ramcl  16730  cshwsiun  16801  cshwrepswhash1  16804  firest  17143  imasvscafn  17248  imasmnd2  18422  dfgrp3lem  18673  imasgrp2  18690  issubg4  18774  cycsubm  18821  gaorber  18914  orbsta  18919  pmtr3ncom  19083  psgnran  19123  odmulg  19163  odbezout  19165  gexdvdsi  19188  sylow1lem3  19205  odcau  19209  sylow2alem1  19222  sylow3lem6  19237  lsmelvalm  19256  efgrelexlemb  19356  efgredeu  19358  cyggeninv  19483  cygctb  19493  cyggexb  19500  dprdssv  19619  dprddisj2  19642  ablfacrplem  19668  pgpfac1lem2  19678  pgpfac1lem5  19682  ringinvnzdiv  19832  imasring  19858  dvdsrcl2  19892  dvdsrmul1  19895  lss1d  20225  lssats2  20262  lspsn  20264  lmhmima  20309  lpiss  20521  dvdsrzring  20683  znunit  20771  znrrg  20773  cygznlem3  20777  frgpcyg  20781  lindfrn  21028  mplcoe5lem  21240  mpfind  21317  gsummoncoe1  21475  mpfpf1  21517  pf1mpf  21518  mat1dimelbas  21620  scmatdmat  21664  scmataddcl  21665  scmatsubcl  21666  scmatmulcl  21667  cpmatacl  21865  chpscmat  21991  tgcl  22119  clsval2  22201  innei  22276  restcld  22323  restcldr  22325  ordtrest2lem  22354  cnprest  22440  lmss  22449  lmcls  22453  lmcnp  22455  isreg2  22528  cmpcovf  22542  cncmp  22543  cmpsub  22551  1stcrest  22604  2ndcrest  22605  1stccnp  22613  restnlly  22633  cldllycmp  22646  locfincmp  22677  txcnpi  22759  pthaus  22789  txtube  22791  txcmplem1  22792  txcmplem2  22793  txlm  22799  xkohaus  22804  xkococnlem  22810  xkococn  22811  kqfvima  22881  kqreglem1  22892  isfild  23009  filuni  23036  isufil2  23059  uffix  23072  rnelfm  23104  fmfnfmlem2  23106  fmfnfmlem4  23108  fmfnfm  23109  fmco  23112  fclsopn  23165  ufilcmp  23183  cnpfcf  23192  alexsublem  23195  alexsubALT  23202  cldsubg  23262  ghmcnp  23266  qustgpopn  23271  tsmsgsum  23290  tsmsres  23295  tsmsxplem1  23304  tsmsxp  23306  isucn2  23431  ucnprima  23434  imasdsf1olem  23526  blssps  23577  blss  23578  blssexps  23579  blssex  23580  mopni3  23650  blcld  23661  metrest  23680  metcnp3  23696  reperflem  23981  icccmplem3  23987  xrge0tsms  23997  mulc1cncf  24068  cncfco  24070  cnheibor  24118  bndth  24121  lebnumlem3  24126  xlebnum  24128  lebnumii  24129  nmhmcn  24283  cfil3i  24433  cmetcaulem  24452  cfilres  24460  bcthlem4  24491  ivthlem2  24616  ivthlem3  24617  ivthicc  24622  cniccbdd  24625  ovolunlem1  24661  ovoliunlem2  24667  ovolshftlem2  24674  ovolicc2  24686  iunmbl2  24721  dyadmax  24762  opnmbllem  24765  subopnmbl  24768  volivth  24771  ismbf3d  24818  mbfimaopn2  24821  mbfaddlem  24824  i1fmullem  24858  mbfi1fseqlem4  24883  bddiblnc  25006  ellimc3  25043  dvlip  25157  dvlip2  25159  c1liplem1  25160  dvgt0lem1  25166  dvivthlem2  25173  dvne0  25175  lhop1lem  25177  lhop2  25179  lhop  25180  tdeglem4  25224  tdeglem4OLD  25225  mdegnn0cl  25236  ply1divex  25301  dvdsq1p  25325  ig1peu  25336  elply2  25357  plypf1  25373  plydivex  25457  aalioulem3  25494  aalioulem5  25496  aaliou  25498  ulmshftlem  25548  ulmcau  25554  ulmss  25556  ulmbdd  25557  ulmcn  25558  radcnvlt1  25577  eflogeq  25757  efopn  25813  cxpeq  25910  angpieqvd  25981  xrlimcnp  26118  cxploglim  26127  ftalem2  26223  ftalem7  26228  isppw2  26264  dchrptlem1  26412  dchrptlem3  26414  dchrsum2  26416  lgsdchrval  26502  lgsdchr  26503  gausslemma2dlem1a  26513  lgsquadlem1  26528  2lgsoddprmlem2  26557  dchrisumlem3  26639  dchrisum0fno1  26659  pntlem3  26757  pntleml  26759  ostth3  26786  brcgr  27268  brbtwn2  27273  axbtwnid  27307  axcontlem7  27338  usgrnloopALT  27570  uhgrspansubgrlem  27657  nbuhgr  27710  nbupgr  27711  wwlksnextprop  28277  elwspths2on  28325  erclwwlktr  28386  clwwlknscsh  28426  erclwwlkntr  28435  hashecclwwlkn1  28441  umgrhashecclwwlk  28442  3cyclfrgrrn1  28649  frgrregorufr  28689  frgr2wwlk1  28693  ubthlem1  29232  ubthlem3  29234  htthlem  29279  omlsii  29765  spansncol  29930  nmopun  30376  nmcexi  30388  riesz1  30427  elpjrn  30552  cvcon3  30646  chcv1  30717  atcvatlem  30747  chirredi  30756  br8d  30950  xrge0tsmsd  31317  ordtrest2NEWlem  31872  lmxrge0  31902  esumfsup  32038  esumpcvgval  32046  measdivcstALTV  32193  eulerpartlemgh  32345  dstfrvunirn  32441  afsval  32651  erdszelem8  33160  erdszelem11  33163  erdsze2lem2  33166  connpconn  33197  sconnpi1  33201  cvmsss2  33236  cvmfolem  33241  cvmliftmolem2  33244  cvmliftlem15  33260  cvmlift2lem1  33264  cvmlift3lem4  33284  cvmlift3lem5  33285  satfdmlem  33330  fmla1  33349  gonarlem  33356  gonar  33357  goalrlem  33358  goalr  33359  fmla0disjsuc  33360  fmlasucdisj  33361  satffunlem1lem1  33364  satffunlem1lem2  33365  satffunlem2lem1  33366  mrsub0  33478  mrsubcn  33481  msubrn  33491  msubvrs  33522  br8  33723  br6  33724  br4  33725  xpord3pred  33798  sexp3  33799  nosupno  33906  nosupbday  33908  noinfbday  33923  scutun12  34004  oldssmade  34060  cgrtriv  34304  btwntriv2  34314  btwncomim  34315  btwnswapid  34319  btwnintr  34321  btwnexch3  34322  btwnouttr2  34324  ifscgr  34346  cgrxfr  34357  btwnxfr  34358  btwnconn3  34405  segcon2  34407  brsegle  34410  seglecgr12im  34412  broutsideof3  34428  linethru  34455  elhf2  34477  opnregcld  34519  cldregopn  34520  neibastop2lem  34549  matunitlindflem1  35773  poimirlem16  35793  poimirlem17  35794  poimirlem19  35796  poimirlem20  35797  poimirlem24  35801  poimirlem29  35806  heicant  35812  opnmbllem0  35813  ismblfin  35818  itg2addnclem  35828  itg2addnclem3  35830  itg2gt0cn  35832  ftc1anclem5  35854  ftc2nc  35859  filbcmb  35898  fdc  35903  incsequz  35906  caushft  35919  istotbnd3  35929  equivbnd  35948  cntotbnd  35954  heibor1lem  35967  heibor1  35968  bfplem2  35981  divrngidl  36186  prnc  36225  lshpdisj  37001  cvrcon3b  37291  atnle  37331  hlhgt2  37403  hl0lt1N  37404  hl2at  37419  cvrexchlem  37433  cvratlem  37435  lvolnlelpln  37599  2lplnj  37634  ispsubcl2N  37961  lautcvr  38106  dva1dim  38999  dib1dim  39179  dib1dim2  39182  diclspsn  39208  dih1dimatlem  39343  dihlatat  39351  dihatexv  39352  dihatexv2  39353  lcfrlem9  39564  lcfrlem16  39572  mapdrvallem2  39659  mapd1o  39662  elre0re  40291  dvdsexpim  40328  prjspner1  40463  dffltz  40471  rexlimdv3d  40505  elrfi  40516  isnacs3  40532  eldiophb  40579  eldiophss  40596  diophren  40635  rencldnfilem  40642  pell1234qrdich  40683  pellfundex  40708  lsmfgcl  40899  kercvrlsm  40908  lmhmfgima  40909  lpirlnr  40942  hbtlem2  40949  hbtlem4  40951  hbtlem6  40954  rngunsnply  40998  restuni3  42667  limsupubuz  43254  stoweidlem57  43598  fourierdlem48  43695  fourierdlem49  43696  sge0le  43945  fsetsniunop  44543  cfsetsnfsetfo  44554  fcoresf1  44563  euoreqb  44601  imasetpreimafvbijlemf1  44856  imasetpreimafvbijlemfo  44857  iccpartrn  44882  iccpartiun  44886  iccpartnel  44890  paireqne  44963  reupr  44974  odz2prm2pw  45015  fmtnofac2lem  45020  prmdvdsfmtnof1lem2  45037  2pwp1prm  45041  mod42tp1mod8  45054  lighneallem3  45059  lighneallem4  45062  requad01  45073  requad2  45075  fppr2odd  45183  gbowpos  45211  gbowgt5  45214  gboge9  45216  nnsum4primesodd  45248  nnsum4primesoddALTV  45249  isomushgr  45278  isomuspgrlem2d  45283  copisnmnd  45363  lidldomn1  45479  affinecomb1  46048  eenglngeehlnmlem2  46084  rrx2vlinest  46087  itsclquadb  46122  rspceb2dv  46148  aacllem  46505