Theorem rexlimdva 3223

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

Syntax hints:   → wi 4   ∧ wa 387   ∈ wcel 2048  ∃wrex 3083

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-ral 3087  df-rex 3088

This theorem is referenced by:  rexlimdvaa  3224  rexlimivv  3231  rexlimdvv  3232  ssexnelpss  3976  ralxfrd2  5160  iunopeqop  5260  elsnxp  5974  foco2  6690  elunirn  6829  f1elima  6840  mpoexw  7577  tfrlem9a  7819  seqomlem2  7883  oawordexr  7975  odi  7998  oelimcl  8019  nnawordex  8056  nnaordex  8057  oaabs  8063  oaabs2  8064  omabs  8066  ectocld  8156  onfin  8496  dif1en  8538  isfinite2  8563  isfiniteg  8565  fofinf1o  8586  elfiun  8681  suplub2  8712  supisoex  8725  ordtypelem9  8777  ordtypelem10  8778  brwdom2  8824  brwdom3  8833  rankr1ai  9013  fodomfi2  9272  infpwfien  9274  dfac12r  9358  ackbij1  9450  cff1  9470  fin23lem21  9551  isf32lem2  9566  fin1a2lem11  9622  fin1a2lem13  9624  ficard  9777  gchina  9911  eltsk2g  9963  tskr1om2  9980  rankcf  9989  inatsk  9990  tskuni  9995  nqereu  10141  ltexnq  10187  1idpr  10241  suplem1pr  10264  supsrlem  10323  axpre-sup  10381  1re  10431  0re  10433  0cnALT  10666  negfi  11382  fiminreOLD  11383  supaddc  11401  supadd  11402  supmul1  11403  supmul  11406  suprzcl2  12145  qmulz  12158  elpq  12182  qbtwnre  12402  ioo0  12572  ico0  12593  ioc0  12594  icc0  12595  addmodlteq  13122  fsequb  13151  hashdom  13546  ccats1alpha  13772  reuccats1lemOLD  13910  reuccatpfxs1lem  13945  shftlem  14278  rexuzre  14563  rexico  14564  caubnd  14569  limsupbnd1  14690  limsupbnd2  14691  rlim2lt  14705  rlim3  14706  lo1bdd2  14732  lo1bddrp  14733  o1lo1  14745  climuni  14760  climshftlem  14782  o1co  14794  rlimcn1  14796  climcn1  14799  o1rlimmul  14826  lo1le  14859  rlimno1  14861  isercoll  14875  caurcvg2  14885  serf0  14888  summolem2  14923  zsum  14925  fsum2dlem  14975  geomulcvg  15082  mertenslem2  15091  ntrivcvg  15103  zprod  15141  fprod2dlem  15184  dvds1lem  15471  odd2np1lem  15539  sqoddm1div8z  15553  ltoddhalfle  15560  halfleoddlt  15561  flodddiv4  15614  dvdssqim  15750  coprmdvds2  15844  divgcdcoprm0  15855  cncongr1  15857  cncongr2  15858  isprm5  15897  rpexp  15910  pythagtriplem1  15999  iserodd  16018  pc2dvds  16061  difsqpwdvds  16069  oddprmdvds  16085  prmpwdvds  16086  4sqlem11  16137  vdwapun  16156  vdwlem2  16164  vdwlem6  16168  vdwlem8  16170  vdwlem10  16172  vdwnnlem1  16177  vdwnnlem3  16179  0ram  16202  ramub1lem2  16209  ramcl  16211  cshwsiun  16279  cshwrepswhash1  16282  firest  16552  imasvscafn  16656  imasmnd2  17785  dfgrp3lem  17974  imasgrp2  17991  issubg4  18072  gaorber  18199  orbsta  18204  pmtr3ncom  18354  psgnran  18395  odmulg  18434  odbezout  18436  gexdvdsi  18459  sylow1lem3  18476  odcau  18480  sylow2alem1  18493  sylow3lem6  18508  lsmelvalm  18527  efgrelexlemb  18626  efgredeu  18628  cyggeninv  18748  cygctb  18756  cyggexb  18763  dprdssv  18878  dprddisj2  18901  ablfacrplem  18927  pgpfac1lem2  18937  pgpfac1lem5  18941  ringinvnzdiv  19056  imasring  19082  dvdsrcl2  19113  dvdsrmul1  19116  lss1d  19447  lssats2  19484  lspsn  19486  lmhmima  19531  lpiss  19734  mplcoe5lem  19951  mpfind  20019  gsummoncoe1  20165  mpfpf1  20206  pf1mpf  20207  dvdsrzring  20322  znunit  20402  znrrg  20404  cygznlem3  20408  frgpcyg  20412  psgnghm  20416  lindfrn  20657  mat1dimelbas  20774  scmatdmat  20818  scmataddcl  20819  scmatsubcl  20820  scmatmulcl  20821  cpmatacl  21018  chpscmat  21144  tgcl  21271  clsval2  21352  innei  21427  restcld  21474  restcldr  21476  ordtrest2lem  21505  cnprest  21591  lmss  21600  lmcls  21604  lmcnp  21606  isreg2  21679  cmpcovf  21693  cncmp  21694  cmpsub  21702  1stcrest  21755  2ndcrest  21756  1stccnp  21764  restnlly  21784  cldllycmp  21797  locfincmp  21828  txcnpi  21910  pthaus  21940  txtube  21942  txcmplem1  21943  txcmplem2  21944  txlm  21950  xkohaus  21955  xkococnlem  21961  xkococn  21962  kqfvima  22032  kqreglem1  22043  isfild  22160  filuni  22187  isufil2  22210  uffix  22223  rnelfm  22255  fmfnfmlem2  22257  fmfnfmlem4  22259  fmfnfm  22260  fmco  22263  fclsopn  22316  ufilcmp  22334  cnpfcf  22343  alexsublem  22346  alexsubALT  22353  cldsubg  22412  ghmcnp  22416  qustgpopn  22421  tsmsgsum  22440  tsmsres  22445  tsmsxplem1  22454  tsmsxp  22456  isucn2  22581  ucnprima  22584  imasdsf1olem  22676  blssps  22727  blss  22728  blssexps  22729  blssex  22730  mopni3  22797  blcld  22808  metrest  22827  metcnp3  22843  reperflem  23119  icccmplem3  23125  xrge0tsms  23135  mulc1cncf  23206  cncfco  23208  cnheibor  23252  bndth  23255  lebnumlem3  23260  xlebnum  23262  lebnumii  23263  nmhmcn  23417  cfil3i  23565  cmetcaulem  23584  cfilres  23592  bcthlem4  23623  ivthlem2  23746  ivthlem3  23747  ivthicc  23752  cniccbdd  23755  ovolunlem1  23791  ovoliunlem2  23797  ovolshftlem2  23804  ovolicc2  23816  iunmbl2  23851  dyadmax  23892  opnmbllem  23895  subopnmbl  23898  volivth  23901  ismbf3d  23948  mbfimaopn2  23951  mbfaddlem  23954  i1fmullem  23988  mbfi1fseqlem4  24012  ellimc3  24170  dvlip  24283  dvlip2  24285  c1liplem1  24286  dvgt0lem1  24292  dvivthlem2  24299  dvne0  24301  lhop1lem  24303  lhop2  24305  lhop  24306  tdeglem4  24347  mdegnn0cl  24358  ply1divex  24423  dvdsq1p  24447  ig1peu  24458  elply2  24479  plypf1  24495  plydivex  24579  aalioulem3  24616  aalioulem5  24618  aaliou  24620  ulmshftlem  24670  ulmcau  24676  ulmss  24678  ulmbdd  24679  ulmcn  24680  radcnvlt1  24699  eflogeq  24876  efopn  24932  cxpeq  25029  angpieqvd  25100  xrlimcnp  25238  cxploglim  25247  ftalem2  25343  ftalem7  25348  isppw2  25384  dchrptlem1  25532  dchrptlem3  25534  dchrsum2  25536  lgsdchrval  25622  lgsdchr  25623  gausslemma2dlem1a  25633  lgsquadlem1  25648  2lgsoddprmlem2  25677  dchrisumlem3  25759  dchrisum0fno1  25779  pntlem3  25877  pntleml  25879  ostth3  25906  brcgr  26379  brbtwn2  26384  axbtwnid  26418  axcontlem7  26449  usgrnloopALT  26678  uhgrspansubgrlem  26765  nbuhgr  26818  nbupgr  26819  wwlksnextprop  27405  wwlksnextpropOLD  27406  elwspths2on  27456  erclwwlktr  27527  clwwlknscsh  27576  erclwwlkntr  27585  hashecclwwlkn1  27591  umgrhashecclwwlk  27592  3cyclfrgrrn1  27809  frgrregorufr  27849  frgr2wwlk1  27853  ubthlem1  28415  ubthlem3  28417  htthlem  28463  omlsii  28951  spansncol  29116  nmopun  29562  nmcexi  29574  riesz1  29613  elpjrn  29738  cvcon3  29832  chcv1  29903  atcvatlem  29933  chirredi  29942  br8d  30115  xrge0tsmsd  30486  ordtrest2NEWlem  30766  lmxrge0  30796  esumfsup  30930  esumpcvgval  30938  measdivcstOLD  31085  eulerpartlemgh  31238  dstfrvunirn  31335  afsval  31551  erdszelem8  31990  erdszelem11  31993  erdsze2lem2  31996  connpconn  32027  sconnpi1  32031  cvmsss2  32066  cvmfolem  32071  cvmliftmolem2  32074  cvmliftlem15  32090  cvmlift2lem1  32094  cvmlift3lem4  32114  cvmlift3lem5  32115  mrsub0  32223  mrsubcn  32226  msubrn  32236  msubvrs  32267  dvdspw  32442  br8  32452  br6  32453  br4  32454  nosupno  32664  nosupbday  32666  scutun12  32732  cgrtriv  32924  btwntriv2  32934  btwncomim  32935  btwnswapid  32939  btwnintr  32941  btwnexch3  32942  btwnouttr2  32944  ifscgr  32966  cgrxfr  32977  btwnxfr  32978  btwnconn3  33025  segcon2  33027  brsegle  33030  seglecgr12im  33032  broutsideof3  33048  linethru  33075  elhf2  33097  opnregcld  33139  cldregopn  33140  neibastop2lem  33169  matunitlindflem1  34277  poimirlem16  34297  poimirlem17  34298  poimirlem19  34300  poimirlem20  34301  poimirlem24  34305  poimirlem29  34310  heicant  34316  opnmbllem0  34317  ismblfin  34322  itg2addnclem  34332  itg2addnclem3  34334  itg2gt0cn  34336  bddiblnc  34351  ftc1anclem5  34360  ftc2nc  34365  filbcmb  34405  fdc  34410  incsequz  34413  caushft  34426  istotbnd3  34439  equivbnd  34458  cntotbnd  34464  heibor1lem  34477  heibor1  34478  bfplem2  34491  divrngidl  34696  prnc  34735  lshpdisj  35516  cvrcon3b  35806  atnle  35846  hlhgt2  35918  hl0lt1N  35919  hl2at  35934  cvrexchlem  35948  cvratlem  35950  lvolnlelpln  36114  2lplnj  36149  ispsubcl2N  36476  lautcvr  36621  dva1dim  37514  dib1dim  37694  dib1dim2  37697  diclspsn  37723  dih1dimatlem  37858  dihlatat  37866  dihatexv  37867  dihatexv2  37868  lcfrlem9  38079  lcfrlem16  38087  mapdrvallem2  38174  mapd1o  38177  elre0re  38536  dvdsexpim  38558  dffltz  38623  elrfi  38631  isnacs3  38647  eldiophb  38694  eldiophss  38712  diophren  38751  rencldnfilem  38758  pell1234qrdich  38799  pellfundex  38824  lsmfgcl  39015  kercvrlsm  39024  lmhmfgima  39025  lpirlnr  39058  hbtlem2  39065  hbtlem4  39067  hbtlem6  39070  rngunsnply  39114  restuni3  40753  limsupubuz  41371  stoweidlem57  41719  fourierdlem48  41816  fourierdlem49  41817  sge0le  42066  euoreqb  42660  iccpartrn  42908  iccpartiun  42912  iccpartnel  42916  paireqne  42981  reupr  42992  odz2prm2pw  43033  fmtnofac2lem  43038  prmdvdsfmtnof1lem2  43055  2pwp1prm  43059  mod42tp1mod8  43075  lighneallem3  43080  lighneallem4  43083  requad01  43094  requad2  43096  fppr2odd  43204  gbowpos  43232  gbowgt5  43235  gboge9  43237  nnsum4primesodd  43269  nnsum4primesoddALTV  43270  isomushgr  43299  isomuspgrlem2d  43304  copisnmnd  43384  lidldomn1  43496  affinecomb1  43997  eenglngeehlnmlem2  44033  rrx2vlinest  44036  itsclquadb  44071  aacllem  44209