Theorem rexlimdva 3284

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114  ∃wrex 3139

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 209  df-an 399  df-ex 1781  df-ral 3143  df-rex 3144

This theorem is referenced by:  rexlimdvaa  3285  rexlimivv  3292  rexlimdvv  3293  ssexnelpss  4090  ralxfrd2  5313  iunopeqop  5411  elsnxp  6142  foco2  6873  elunirn  7010  f1elima  7021  releldmdifi  7744  mpoexw  7776  tfrlem9a  8022  seqomlem2  8087  oawordexr  8182  odi  8205  oelimcl  8226  nnawordex  8263  nnaordex  8264  oaabs  8271  oaabs2  8272  omabs  8274  ectocld  8364  onfin  8709  dif1en  8751  isfinite2  8776  isfiniteg  8778  fofinf1o  8799  elfiun  8894  suplub2  8925  supisoex  8938  ordtypelem9  8990  ordtypelem10  8991  brwdom2  9037  brwdom3  9046  rankr1ai  9227  fodomfi2  9486  infpwfien  9488  dfac12r  9572  ackbij1  9660  cff1  9680  fin23lem21  9761  isf32lem2  9776  fin1a2lem11  9832  fin1a2lem13  9834  ficard  9987  gchina  10121  eltsk2g  10173  tskr1om2  10190  rankcf  10199  inatsk  10200  tskuni  10205  nqereu  10351  ltexnq  10397  1idpr  10451  suplem1pr  10474  supsrlem  10533  axpre-sup  10591  1re  10641  0re  10643  0cnALT  10874  negfi  11589  fiminreOLD  11590  supaddc  11608  supadd  11609  supmul1  11610  supmul  11613  suprzcl2  12339  qmulz  12352  elpq  12375  qbtwnre  12593  ioo0  12764  ico0  12785  ioc0  12786  icc0  12787  addmodlteq  13315  fsequb  13344  hashdom  13741  ccats1alpha  13973  reuccatpfxs1lem  14108  shftlem  14427  rexuzre  14712  rexico  14713  caubnd  14718  limsupbnd1  14839  limsupbnd2  14840  rlim2lt  14854  rlim3  14855  lo1bdd2  14881  lo1bddrp  14882  o1lo1  14894  climuni  14909  climshftlem  14931  o1co  14943  rlimcn1  14945  climcn1  14948  o1rlimmul  14975  lo1le  15008  rlimno1  15010  isercoll  15024  caurcvg2  15034  serf0  15037  summolem2  15073  zsum  15075  fsum2dlem  15125  geomulcvg  15232  mertenslem2  15241  ntrivcvg  15253  zprod  15291  fprod2dlem  15334  dvds1lem  15621  odd2np1lem  15689  sqoddm1div8z  15703  ltoddhalfle  15710  halfleoddlt  15711  flodddiv4  15764  dvdssqim  15904  coprmdvds2  15998  divgcdcoprm0  16009  cncongr1  16011  cncongr2  16012  isprm5  16051  rpexp  16064  pythagtriplem1  16153  iserodd  16172  pc2dvds  16215  difsqpwdvds  16223  oddprmdvds  16239  prmpwdvds  16240  4sqlem11  16291  vdwapun  16310  vdwlem2  16318  vdwlem6  16322  vdwlem8  16324  vdwlem10  16326  vdwnnlem1  16331  vdwnnlem3  16333  0ram  16356  ramub1lem2  16363  ramcl  16365  cshwsiun  16433  cshwrepswhash1  16436  firest  16706  imasvscafn  16810  imasmnd2  17948  dfgrp3lem  18197  imasgrp2  18214  issubg4  18298  cycsubm  18345  gaorber  18438  orbsta  18443  pmtr3ncom  18603  psgnran  18643  odmulg  18683  odbezout  18685  gexdvdsi  18708  sylow1lem3  18725  odcau  18729  sylow2alem1  18742  sylow3lem6  18757  lsmelvalm  18776  efgrelexlemb  18876  efgredeu  18878  cyggeninv  19002  cygctb  19012  cyggexb  19019  dprdssv  19138  dprddisj2  19161  ablfacrplem  19187  pgpfac1lem2  19197  pgpfac1lem5  19201  ringinvnzdiv  19343  imasring  19369  dvdsrcl2  19400  dvdsrmul1  19403  lss1d  19735  lssats2  19772  lspsn  19774  lmhmima  19819  lpiss  20023  mplcoe5lem  20248  mpfind  20320  gsummoncoe1  20472  mpfpf1  20514  pf1mpf  20515  dvdsrzring  20630  znunit  20710  znrrg  20712  cygznlem3  20716  frgpcyg  20720  lindfrn  20965  mat1dimelbas  21080  scmatdmat  21124  scmataddcl  21125  scmatsubcl  21126  scmatmulcl  21127  cpmatacl  21324  chpscmat  21450  tgcl  21577  clsval2  21658  innei  21733  restcld  21780  restcldr  21782  ordtrest2lem  21811  cnprest  21897  lmss  21906  lmcls  21910  lmcnp  21912  isreg2  21985  cmpcovf  21999  cncmp  22000  cmpsub  22008  1stcrest  22061  2ndcrest  22062  1stccnp  22070  restnlly  22090  cldllycmp  22103  locfincmp  22134  txcnpi  22216  pthaus  22246  txtube  22248  txcmplem1  22249  txcmplem2  22250  txlm  22256  xkohaus  22261  xkococnlem  22267  xkococn  22268  kqfvima  22338  kqreglem1  22349  isfild  22466  filuni  22493  isufil2  22516  uffix  22529  rnelfm  22561  fmfnfmlem2  22563  fmfnfmlem4  22565  fmfnfm  22566  fmco  22569  fclsopn  22622  ufilcmp  22640  cnpfcf  22649  alexsublem  22652  alexsubALT  22659  cldsubg  22719  ghmcnp  22723  qustgpopn  22728  tsmsgsum  22747  tsmsres  22752  tsmsxplem1  22761  tsmsxp  22763  isucn2  22888  ucnprima  22891  imasdsf1olem  22983  blssps  23034  blss  23035  blssexps  23036  blssex  23037  mopni3  23104  blcld  23115  metrest  23134  metcnp3  23150  reperflem  23426  icccmplem3  23432  xrge0tsms  23442  mulc1cncf  23513  cncfco  23515  cnheibor  23559  bndth  23562  lebnumlem3  23567  xlebnum  23569  lebnumii  23570  nmhmcn  23724  cfil3i  23872  cmetcaulem  23891  cfilres  23899  bcthlem4  23930  ivthlem2  24053  ivthlem3  24054  ivthicc  24059  cniccbdd  24062  ovolunlem1  24098  ovoliunlem2  24104  ovolshftlem2  24111  ovolicc2  24123  iunmbl2  24158  dyadmax  24199  opnmbllem  24202  subopnmbl  24205  volivth  24208  ismbf3d  24255  mbfimaopn2  24258  mbfaddlem  24261  i1fmullem  24295  mbfi1fseqlem4  24319  ellimc3  24477  dvlip  24590  dvlip2  24592  c1liplem1  24593  dvgt0lem1  24599  dvivthlem2  24606  dvne0  24608  lhop1lem  24610  lhop2  24612  lhop  24613  tdeglem4  24654  mdegnn0cl  24665  ply1divex  24730  dvdsq1p  24754  ig1peu  24765  elply2  24786  plypf1  24802  plydivex  24886  aalioulem3  24923  aalioulem5  24925  aaliou  24927  ulmshftlem  24977  ulmcau  24983  ulmss  24985  ulmbdd  24986  ulmcn  24987  radcnvlt1  25006  eflogeq  25185  efopn  25241  cxpeq  25338  angpieqvd  25409  xrlimcnp  25546  cxploglim  25555  ftalem2  25651  ftalem7  25656  isppw2  25692  dchrptlem1  25840  dchrptlem3  25842  dchrsum2  25844  lgsdchrval  25930  lgsdchr  25931  gausslemma2dlem1a  25941  lgsquadlem1  25956  2lgsoddprmlem2  25985  dchrisumlem3  26067  dchrisum0fno1  26087  pntlem3  26185  pntleml  26187  ostth3  26214  brcgr  26686  brbtwn2  26691  axbtwnid  26725  axcontlem7  26756  usgrnloopALT  26985  uhgrspansubgrlem  27072  nbuhgr  27125  nbupgr  27126  wwlksnextprop  27691  elwspths2on  27739  erclwwlktr  27800  clwwlknscsh  27841  erclwwlkntr  27850  hashecclwwlkn1  27856  umgrhashecclwwlk  27857  3cyclfrgrrn1  28064  frgrregorufr  28104  frgr2wwlk1  28108  ubthlem1  28647  ubthlem3  28649  htthlem  28694  omlsii  29180  spansncol  29345  nmopun  29791  nmcexi  29803  riesz1  29842  elpjrn  29967  cvcon3  30061  chcv1  30132  atcvatlem  30162  chirredi  30171  br8d  30361  xrge0tsmsd  30692  ordtrest2NEWlem  31165  lmxrge0  31195  esumfsup  31329  esumpcvgval  31337  measdivcstALTV  31484  eulerpartlemgh  31636  dstfrvunirn  31732  afsval  31942  erdszelem8  32445  erdszelem11  32448  erdsze2lem2  32451  connpconn  32482  sconnpi1  32486  cvmsss2  32521  cvmfolem  32526  cvmliftmolem2  32529  cvmliftlem15  32545  cvmlift2lem1  32549  cvmlift3lem4  32569  cvmlift3lem5  32570  satfdmlem  32615  fmla1  32634  gonarlem  32641  gonar  32642  goalrlem  32643  goalr  32644  fmla0disjsuc  32645  fmlasucdisj  32646  satffunlem1lem1  32649  satffunlem1lem2  32650  satffunlem2lem1  32651  mrsub0  32763  mrsubcn  32766  msubrn  32776  msubvrs  32807  dvdspw  32982  br8  32992  br6  32993  br4  32994  nosupno  33203  nosupbday  33205  scutun12  33271  cgrtriv  33463  btwntriv2  33473  btwncomim  33474  btwnswapid  33478  btwnintr  33480  btwnexch3  33481  btwnouttr2  33483  ifscgr  33505  cgrxfr  33516  btwnxfr  33517  btwnconn3  33564  segcon2  33566  brsegle  33569  seglecgr12im  33571  broutsideof3  33587  linethru  33614  elhf2  33636  opnregcld  33678  cldregopn  33679  neibastop2lem  33708  matunitlindflem1  34903  poimirlem16  34923  poimirlem17  34924  poimirlem19  34926  poimirlem20  34927  poimirlem24  34931  poimirlem29  34936  heicant  34942  opnmbllem0  34943  ismblfin  34948  itg2addnclem  34958  itg2addnclem3  34960  itg2gt0cn  34962  bddiblnc  34977  ftc1anclem5  34986  ftc2nc  34991  filbcmb  35030  fdc  35035  incsequz  35038  caushft  35051  istotbnd3  35064  equivbnd  35083  cntotbnd  35089  heibor1lem  35102  heibor1  35103  bfplem2  35116  divrngidl  35321  prnc  35360  lshpdisj  36138  cvrcon3b  36428  atnle  36468  hlhgt2  36540  hl0lt1N  36541  hl2at  36556  cvrexchlem  36570  cvratlem  36572  lvolnlelpln  36736  2lplnj  36771  ispsubcl2N  37098  lautcvr  37243  dva1dim  38136  dib1dim  38316  dib1dim2  38319  diclspsn  38345  dih1dimatlem  38480  dihlatat  38488  dihatexv  38489  dihatexv2  38490  lcfrlem9  38701  lcfrlem16  38709  mapdrvallem2  38796  mapd1o  38799  elre0re  39174  dvdsexpim  39201  dffltz  39291  rexlimdv3d  39300  elrfi  39311  isnacs3  39327  eldiophb  39374  eldiophss  39391  diophren  39430  rencldnfilem  39437  pell1234qrdich  39478  pellfundex  39503  lsmfgcl  39694  kercvrlsm  39703  lmhmfgima  39704  lpirlnr  39737  hbtlem2  39744  hbtlem4  39746  hbtlem6  39749  rngunsnply  39793  restuni3  41404  limsupubuz  42014  stoweidlem57  42362  fourierdlem48  42459  fourierdlem49  42460  sge0le  42709  euoreqb  43328  imasetpreimafvbijlemf1  43584  imasetpreimafvbijlemfo  43585  iccpartrn  43610  iccpartiun  43614  iccpartnel  43618  paireqne  43693  reupr  43704  odz2prm2pw  43745  fmtnofac2lem  43750  prmdvdsfmtnof1lem2  43767  2pwp1prm  43771  mod42tp1mod8  43787  lighneallem3  43792  lighneallem4  43795  requad01  43806  requad2  43808  fppr2odd  43916  gbowpos  43944  gbowgt5  43947  gboge9  43949  nnsum4primesodd  43981  nnsum4primesoddALTV  43982  isomushgr  44011  isomuspgrlem2d  44016  copisnmnd  44096  lidldomn1  44212  affinecomb1  44709  eenglngeehlnmlem2  44745  rrx2vlinest  44748  itsclquadb  44783  aacllem  44922