Theorem rexlimdva 3212

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-ral 3068  df-rex 3069

This theorem is referenced by:  rexlimdvaa  3213  rexlimivv  3220  rexlimdvv  3221  ssexnelpss  4044  ralxfrd2  5330  iunopeqop  5429  elsnxp  6183  foco2  6965  elunirn  7106  f1elima  7117  releldmdifi  7859  mpoexw  7892  tfrlem9a  8188  seqomlem2  8252  oawordexr  8349  odi  8372  oelimcl  8393  nnawordex  8430  nnaordex  8431  oaabs  8438  oaabs2  8439  omabs  8441  ectocld  8531  onfin  8944  dif1enALT  8980  isfinite2  9002  isfiniteg  9004  fofinf1o  9024  elfiun  9119  suplub2  9150  supisoex  9163  ordtypelem9  9215  ordtypelem10  9216  brwdom2  9262  brwdom3  9271  rankr1ai  9487  fodomfi2  9747  infpwfien  9749  dfac12r  9833  ackbij1  9925  cff1  9945  fin23lem21  10026  isf32lem2  10041  fin1a2lem11  10097  fin1a2lem13  10099  ficard  10252  gchina  10386  eltsk2g  10438  tskr1om2  10455  rankcf  10464  inatsk  10465  tskuni  10470  nqereu  10616  ltexnq  10662  1idpr  10716  suplem1pr  10739  supsrlem  10798  axpre-sup  10856  1re  10906  0re  10908  0cnALT  11139  negfi  11854  supaddc  11872  supadd  11873  supmul1  11874  supmul  11877  suprzcl2  12607  qmulz  12620  elpq  12644  qbtwnre  12862  ioo0  13033  ico0  13054  ioc0  13055  icc0  13056  addmodlteq  13594  fsequb  13623  hashdom  14022  ccats1alpha  14252  reuccatpfxs1lem  14387  shftlem  14707  rexuzre  14992  rexico  14993  caubnd  14998  limsupbnd1  15119  limsupbnd2  15120  rlim2lt  15134  rlim3  15135  lo1bdd2  15161  lo1bddrp  15162  o1lo1  15174  climuni  15189  climshftlem  15211  o1co  15223  rlimcn1  15225  climcn1  15229  o1rlimmul  15256  lo1le  15291  rlimno1  15293  isercoll  15307  caurcvg2  15317  serf0  15320  summolem2  15356  zsum  15358  fsum2dlem  15410  geomulcvg  15516  mertenslem2  15525  ntrivcvg  15537  zprod  15575  fprod2dlem  15618  dvds1lem  15905  dvdsexp2im  15964  odd2np1lem  15977  sqoddm1div8z  15991  ltoddhalfle  15998  halfleoddlt  15999  flodddiv4  16050  dvdssqim  16192  coprmdvds2  16287  divgcdcoprm0  16298  cncongr1  16300  cncongr2  16301  isprm5  16340  rpexp  16355  pythagtriplem1  16445  iserodd  16464  pc2dvds  16508  difsqpwdvds  16516  oddprmdvds  16532  prmpwdvds  16533  4sqlem11  16584  vdwapun  16603  vdwlem2  16611  vdwlem6  16615  vdwlem8  16617  vdwlem10  16619  vdwnnlem1  16624  vdwnnlem3  16626  0ram  16649  ramub1lem2  16656  ramcl  16658  cshwsiun  16729  cshwrepswhash1  16732  firest  17060  imasvscafn  17165  imasmnd2  18337  dfgrp3lem  18588  imasgrp2  18605  issubg4  18689  cycsubm  18736  gaorber  18829  orbsta  18834  pmtr3ncom  18998  psgnran  19038  odmulg  19078  odbezout  19080  gexdvdsi  19103  sylow1lem3  19120  odcau  19124  sylow2alem1  19137  sylow3lem6  19152  lsmelvalm  19171  efgrelexlemb  19271  efgredeu  19273  cyggeninv  19398  cygctb  19408  cyggexb  19415  dprdssv  19534  dprddisj2  19557  ablfacrplem  19583  pgpfac1lem2  19593  pgpfac1lem5  19597  ringinvnzdiv  19747  imasring  19773  dvdsrcl2  19807  dvdsrmul1  19810  lss1d  20140  lssats2  20177  lspsn  20179  lmhmima  20224  lpiss  20434  dvdsrzring  20595  znunit  20683  znrrg  20685  cygznlem3  20689  frgpcyg  20693  lindfrn  20938  mplcoe5lem  21150  mpfind  21227  gsummoncoe1  21385  mpfpf1  21427  pf1mpf  21428  mat1dimelbas  21528  scmatdmat  21572  scmataddcl  21573  scmatsubcl  21574  scmatmulcl  21575  cpmatacl  21773  chpscmat  21899  tgcl  22027  clsval2  22109  innei  22184  restcld  22231  restcldr  22233  ordtrest2lem  22262  cnprest  22348  lmss  22357  lmcls  22361  lmcnp  22363  isreg2  22436  cmpcovf  22450  cncmp  22451  cmpsub  22459  1stcrest  22512  2ndcrest  22513  1stccnp  22521  restnlly  22541  cldllycmp  22554  locfincmp  22585  txcnpi  22667  pthaus  22697  txtube  22699  txcmplem1  22700  txcmplem2  22701  txlm  22707  xkohaus  22712  xkococnlem  22718  xkococn  22719  kqfvima  22789  kqreglem1  22800  isfild  22917  filuni  22944  isufil2  22967  uffix  22980  rnelfm  23012  fmfnfmlem2  23014  fmfnfmlem4  23016  fmfnfm  23017  fmco  23020  fclsopn  23073  ufilcmp  23091  cnpfcf  23100  alexsublem  23103  alexsubALT  23110  cldsubg  23170  ghmcnp  23174  qustgpopn  23179  tsmsgsum  23198  tsmsres  23203  tsmsxplem1  23212  tsmsxp  23214  isucn2  23339  ucnprima  23342  imasdsf1olem  23434  blssps  23485  blss  23486  blssexps  23487  blssex  23488  mopni3  23556  blcld  23567  metrest  23586  metcnp3  23602  reperflem  23887  icccmplem3  23893  xrge0tsms  23903  mulc1cncf  23974  cncfco  23976  cnheibor  24024  bndth  24027  lebnumlem3  24032  xlebnum  24034  lebnumii  24035  nmhmcn  24189  cfil3i  24338  cmetcaulem  24357  cfilres  24365  bcthlem4  24396  ivthlem2  24521  ivthlem3  24522  ivthicc  24527  cniccbdd  24530  ovolunlem1  24566  ovoliunlem2  24572  ovolshftlem2  24579  ovolicc2  24591  iunmbl2  24626  dyadmax  24667  opnmbllem  24670  subopnmbl  24673  volivth  24676  ismbf3d  24723  mbfimaopn2  24726  mbfaddlem  24729  i1fmullem  24763  mbfi1fseqlem4  24788  bddiblnc  24911  ellimc3  24948  dvlip  25062  dvlip2  25064  c1liplem1  25065  dvgt0lem1  25071  dvivthlem2  25078  dvne0  25080  lhop1lem  25082  lhop2  25084  lhop  25085  tdeglem4  25129  tdeglem4OLD  25130  mdegnn0cl  25141  ply1divex  25206  dvdsq1p  25230  ig1peu  25241  elply2  25262  plypf1  25278  plydivex  25362  aalioulem3  25399  aalioulem5  25401  aaliou  25403  ulmshftlem  25453  ulmcau  25459  ulmss  25461  ulmbdd  25462  ulmcn  25463  radcnvlt1  25482  eflogeq  25662  efopn  25718  cxpeq  25815  angpieqvd  25886  xrlimcnp  26023  cxploglim  26032  ftalem2  26128  ftalem7  26133  isppw2  26169  dchrptlem1  26317  dchrptlem3  26319  dchrsum2  26321  lgsdchrval  26407  lgsdchr  26408  gausslemma2dlem1a  26418  lgsquadlem1  26433  2lgsoddprmlem2  26462  dchrisumlem3  26544  dchrisum0fno1  26564  pntlem3  26662  pntleml  26664  ostth3  26691  brcgr  27171  brbtwn2  27176  axbtwnid  27210  axcontlem7  27241  usgrnloopALT  27473  uhgrspansubgrlem  27560  nbuhgr  27613  nbupgr  27614  wwlksnextprop  28178  elwspths2on  28226  erclwwlktr  28287  clwwlknscsh  28327  erclwwlkntr  28336  hashecclwwlkn1  28342  umgrhashecclwwlk  28343  3cyclfrgrrn1  28550  frgrregorufr  28590  frgr2wwlk1  28594  ubthlem1  29133  ubthlem3  29135  htthlem  29180  omlsii  29666  spansncol  29831  nmopun  30277  nmcexi  30289  riesz1  30328  elpjrn  30453  cvcon3  30547  chcv1  30618  atcvatlem  30648  chirredi  30657  br8d  30851  xrge0tsmsd  31219  ordtrest2NEWlem  31774  lmxrge0  31804  esumfsup  31938  esumpcvgval  31946  measdivcstALTV  32093  eulerpartlemgh  32245  dstfrvunirn  32341  afsval  32551  erdszelem8  33060  erdszelem11  33063  erdsze2lem2  33066  connpconn  33097  sconnpi1  33101  cvmsss2  33136  cvmfolem  33141  cvmliftmolem2  33144  cvmliftlem15  33160  cvmlift2lem1  33164  cvmlift3lem4  33184  cvmlift3lem5  33185  satfdmlem  33230  fmla1  33249  gonarlem  33256  gonar  33257  goalrlem  33258  goalr  33259  fmla0disjsuc  33260  fmlasucdisj  33261  satffunlem1lem1  33264  satffunlem1lem2  33265  satffunlem2lem1  33266  mrsub0  33378  mrsubcn  33381  msubrn  33391  msubvrs  33422  eldifsucnn  33597  br8  33629  br6  33630  br4  33631  ttrcltr  33702  xpord3pred  33725  sexp3  33726  nosupno  33833  nosupbday  33835  noinfbday  33850  scutun12  33931  oldssmade  33987  cgrtriv  34231  btwntriv2  34241  btwncomim  34242  btwnswapid  34246  btwnintr  34248  btwnexch3  34249  btwnouttr2  34251  ifscgr  34273  cgrxfr  34284  btwnxfr  34285  btwnconn3  34332  segcon2  34334  brsegle  34337  seglecgr12im  34339  broutsideof3  34355  linethru  34382  elhf2  34404  opnregcld  34446  cldregopn  34447  neibastop2lem  34476  matunitlindflem1  35700  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem24  35728  poimirlem29  35733  heicant  35739  opnmbllem0  35740  ismblfin  35745  itg2addnclem  35755  itg2addnclem3  35757  itg2gt0cn  35759  ftc1anclem5  35781  ftc2nc  35786  filbcmb  35825  fdc  35830  incsequz  35833  caushft  35846  istotbnd3  35856  equivbnd  35875  cntotbnd  35881  heibor1lem  35894  heibor1  35895  bfplem2  35908  divrngidl  36113  prnc  36152  lshpdisj  36928  cvrcon3b  37218  atnle  37258  hlhgt2  37330  hl0lt1N  37331  hl2at  37346  cvrexchlem  37360  cvratlem  37362  lvolnlelpln  37526  2lplnj  37561  ispsubcl2N  37888  lautcvr  38033  dva1dim  38926  dib1dim  39106  dib1dim2  39109  diclspsn  39135  dih1dimatlem  39270  dihlatat  39278  dihatexv  39279  dihatexv2  39280  lcfrlem9  39491  lcfrlem16  39499  mapdrvallem2  39586  mapd1o  39589  elre0re  40212  dvdsexpim  40249  prjspner1  40384  dffltz  40387  rexlimdv3d  40421  elrfi  40432  isnacs3  40448  eldiophb  40495  eldiophss  40512  diophren  40551  rencldnfilem  40558  pell1234qrdich  40599  pellfundex  40624  lsmfgcl  40815  kercvrlsm  40824  lmhmfgima  40825  lpirlnr  40858  hbtlem2  40865  hbtlem4  40867  hbtlem6  40870  rngunsnply  40914  restuni3  42556  limsupubuz  43144  stoweidlem57  43488  fourierdlem48  43585  fourierdlem49  43586  sge0le  43835  fsetsniunop  44430  cfsetsnfsetfo  44441  fcoresf1  44450  euoreqb  44488  imasetpreimafvbijlemf1  44744  imasetpreimafvbijlemfo  44745  iccpartrn  44770  iccpartiun  44774  iccpartnel  44778  paireqne  44851  reupr  44862  odz2prm2pw  44903  fmtnofac2lem  44908  prmdvdsfmtnof1lem2  44925  2pwp1prm  44929  mod42tp1mod8  44942  lighneallem3  44947  lighneallem4  44950  requad01  44961  requad2  44963  fppr2odd  45071  gbowpos  45099  gbowgt5  45102  gboge9  45104  nnsum4primesodd  45136  nnsum4primesoddALTV  45137  isomushgr  45166  isomuspgrlem2d  45171  copisnmnd  45251  lidldomn1  45367  affinecomb1  45936  eenglngeehlnmlem2  45972  rrx2vlinest  45975  itsclquadb  46010  rspceb2dv  46036  aacllem  46391