Theorem rexlimdva 3133

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  ∃wrex 3056

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 207  df-an 396  df-ex 1781  df-rex 3057

This theorem is referenced by:  rexlimdvaa  3134  rexlimivv  3174  rexlimdvv  3188  rspceb2dv  3581  ssexnelpss  4066  ralxfrd2  5350  iunopeqop  5461  elsnxp  6238  foco2  7042  elunirn  7185  f1elima  7197  mptcnfimad  7918  releldmdifi  7977  mpoexw  8010  xpord3pred  8082  sexp3  8083  tfrlem9a  8305  seqomlem2  8370  oawordexr  8471  odi  8494  oelimcl  8515  nnawordex  8552  nnaordex  8553  oaabs  8563  oaabs2  8564  omabs  8566  eldifsucnn  8579  coflton  8586  cofon1  8587  cofon2  8588  cofonr  8589  naddunif  8608  ectocld  8706  onfin  9124  dif1ennnALT  9161  isfinite2  9182  isfiniteg  9184  fofinf1o  9216  elfiun  9314  suplub2  9345  supisoex  9359  ordtypelem9  9412  ordtypelem10  9413  brwdom2  9459  brwdom3  9468  ttrcltr  9606  rankr1ai  9688  fodomfi2  9948  infpwfien  9950  dfac12r  10035  ackbij1  10125  cff1  10146  fin23lem21  10227  isf32lem2  10242  fin1a2lem11  10298  fin1a2lem13  10300  ficard  10453  gchina  10587  eltsk2g  10639  tskr1om2  10656  rankcf  10665  inatsk  10666  tskuni  10671  nqereu  10817  ltexnq  10863  1idpr  10917  suplem1pr  10940  supsrlem  10999  axpre-sup  11057  1re  11109  0re  11111  0cnALT  11345  supaddc  12086  supadd  12087  supmul1  12088  supmul  12091  suprzcl2  12833  qmulz  12846  elpq  12870  qbtwnre  13095  ioo0  13267  ico0  13288  ioc0  13289  icc0  13290  addmodlteq  13850  fsequb  13879  hashdom  14283  ccats1alpha  14524  reuccatpfxs1lem  14650  shftlem  14972  rexuzre  15257  rexico  15258  caubnd  15263  limsupbnd1  15386  limsupbnd2  15387  rlim2lt  15401  rlim3  15402  lo1bdd2  15428  lo1bddrp  15429  o1lo1  15441  climuni  15456  climshftlem  15478  o1co  15490  rlimcn1  15492  climcn1  15496  o1rlimmul  15523  lo1le  15556  rlimno1  15558  isercoll  15572  caurcvg2  15582  serf0  15585  summolem2  15620  zsum  15622  fsum2dlem  15674  geomulcvg  15780  mertenslem2  15789  ntrivcvg  15801  zprod  15841  fprod2dlem  15884  dvds1lem  16175  dvdsexp2im  16235  odd2np1lem  16248  sqoddm1div8z  16262  ltoddhalfle  16269  halfleoddlt  16270  flodddiv4  16323  dvdssqim  16462  dvdsexpim  16463  coprmdvds2  16562  divgcdcoprm0  16573  cncongr1  16575  cncongr2  16576  isprm5  16615  rpexp  16630  pythagtriplem1  16725  iserodd  16744  pc2dvds  16788  difsqpwdvds  16796  oddprmdvds  16812  prmpwdvds  16813  4sqlem11  16864  vdwapun  16883  vdwlem2  16891  vdwlem6  16895  vdwlem8  16897  vdwlem10  16899  vdwnnlem1  16904  vdwnnlem3  16906  0ram  16929  ramub1lem2  16936  ramcl  16938  cshwsiun  17008  cshwrepswhash1  17011  firest  17333  imasvscafn  17438  imasmnd2  18679  dfgrp3lem  18948  imasgrp2  18965  issubg4  19055  cycsubm  19112  gaorber  19218  orbsta  19223  pmtr3ncom  19385  psgnran  19425  odmulg  19466  odbezout  19468  gexdvdsi  19493  sylow1lem3  19510  odcau  19514  sylow2alem1  19527  sylow3lem6  19542  lsmelvalm  19561  efgrelexlemb  19660  efgredeu  19662  imasabl  19786  cyggeninv  19793  cygctb  19802  cyggexb  19809  dprdssv  19928  dprddisj2  19951  ablfacrplem  19977  pgpfac1lem2  19987  pgpfac1lem5  19991  ringinvnzdiv  20217  imasring  20246  dvdsrcl2  20282  dvdsrmul1  20285  lss1d  20894  lssats2  20931  lspsn  20933  lmhmima  20979  ring2idlqusb  21245  rngqiprngfulem2  21247  lpiss  21264  dvdsrzring  21396  pzriprnglem5  21420  pzriprnglem8  21423  pzriprnglem10  21425  pzriprnglem11  21426  znunit  21498  znrrg  21500  cygznlem3  21504  frgpcyg  21508  lindfrn  21756  mplcoe5lem  21972  mpfind  22040  gsummoncoe1  22221  mpfpf1  22264  pf1mpf  22265  mat1dimelbas  22384  scmatdmat  22428  scmataddcl  22429  scmatsubcl  22430  scmatmulcl  22431  cpmatacl  22629  chpscmat  22755  tgcl  22882  clsval2  22963  innei  23038  restcld  23085  restcldr  23087  ordtrest2lem  23116  cnprest  23202  lmss  23211  lmcls  23215  lmcnp  23217  isreg2  23290  cmpcovf  23304  cncmp  23305  cmpsub  23313  1stcrest  23366  2ndcrest  23367  1stccnp  23375  restnlly  23395  cldllycmp  23408  locfincmp  23439  txcnpi  23521  pthaus  23551  txtube  23553  txcmplem1  23554  txcmplem2  23555  txlm  23561  xkohaus  23566  xkococnlem  23572  xkococn  23573  kqfvima  23643  kqreglem1  23654  isfild  23771  filuni  23798  isufil2  23821  uffix  23834  rnelfm  23866  fmfnfmlem2  23868  fmfnfmlem4  23870  fmfnfm  23871  fmco  23874  fclsopn  23927  ufilcmp  23945  cnpfcf  23954  alexsublem  23957  alexsubALT  23964  cldsubg  24024  ghmcnp  24028  qustgpopn  24033  tsmsgsum  24052  tsmsres  24057  tsmsxplem1  24066  tsmsxp  24068  isucn2  24191  ucnprima  24194  imasdsf1olem  24286  blssps  24337  blss  24338  blssexps  24339  blssex  24340  mopni3  24407  blcld  24418  metrest  24437  metcnp3  24453  reperflem  24732  icccmplem3  24738  xrge0tsms  24748  mulc1cncf  24823  cncfco  24825  cnheibor  24879  bndth  24882  lebnumlem3  24887  xlebnum  24889  lebnumii  24890  nmhmcn  25045  cfil3i  25194  cmetcaulem  25213  cfilres  25221  bcthlem4  25252  ivthlem2  25378  ivthlem3  25379  ivthicc  25384  cniccbdd  25387  ovolunlem1  25423  ovoliunlem2  25429  ovolshftlem2  25436  ovolicc2  25448  iunmbl2  25483  dyadmax  25524  opnmbllem  25527  subopnmbl  25530  volivth  25533  ismbf3d  25580  mbfimaopn2  25583  mbfaddlem  25586  i1fmullem  25620  mbfi1fseqlem4  25644  bddiblnc  25768  ellimc3  25805  dvlip  25923  dvlip2  25925  c1liplem1  25926  dvgt0lem1  25932  dvivthlem2  25939  dvne0  25941  lhop1lem  25943  lhop2  25945  lhop  25946  tdeglem4  25990  mdegnn0cl  26001  ply1divex  26067  dvdsq1p  26093  ig1peu  26105  elply2  26126  plypf1  26142  plydivex  26230  aalioulem3  26267  aalioulem5  26269  aaliou  26271  ulmshftlem  26323  ulmcau  26329  ulmss  26331  ulmbdd  26332  ulmcn  26333  radcnvlt1  26352  eflogeq  26536  efopn  26592  cxpeq  26692  angpieqvd  26766  xrlimcnp  26903  cxploglim  26913  ftalem2  27009  ftalem7  27014  isppw2  27050  dchrptlem1  27200  dchrptlem3  27202  dchrsum2  27204  lgsdchrval  27290  lgsdchr  27291  gausslemma2dlem1a  27301  lgsquadlem1  27316  2lgsoddprmlem2  27345  dchrisumlem3  27427  dchrisum0fno1  27447  pntlem3  27545  pntleml  27547  ostth3  27574  nosupno  27640  nosupbday  27642  noinfbday  27657  scutun12  27749  oldssmade  27820  addsproplem2  27911  addsuniflem  27942  addsbdaylem  27957  negsid  27981  negsunif  27995  precsexlem6  28148  precsexlem7  28149  precsexlem11  28153  bdayon  28207  onaddscl  28208  om2noseqlt  28227  noseqrdgfn  28234  n0sfincut  28280  bdayn0sf1o  28293  dfnns2  28295  zs12negscl  28386  zs12zodd  28390  zs12bday  28392  recut  28396  brcgr  28876  brbtwn2  28881  axbtwnid  28915  axcontlem7  28946  usgrnloopALT  29179  uhgrspansubgrlem  29266  nbuhgr  29319  nbupgr  29320  wwlksnextprop  29888  elwspths2on  29936  erclwwlktr  29997  clwwlknscsh  30037  erclwwlkntr  30046  hashecclwwlkn1  30052  umgrhashecclwwlk  30053  3cyclfrgrrn1  30260  frgrregorufr  30300  frgr2wwlk1  30304  ubthlem1  30845  ubthlem3  30847  htthlem  30892  omlsii  31378  spansncol  31543  nmopun  31989  nmcexi  32001  riesz1  32040  elpjrn  32165  cvcon3  32259  chcv1  32330  atcvatlem  32360  chirredi  32369  br8d  32586  xrge0tsmsd  33037  ordtrest2NEWlem  33930  lmxrge0  33960  esumfsup  34078  esumpcvgval  34086  measdivcstALTV  34233  eulerpartlemgh  34386  dstfrvunirn  34483  afsval  34679  onvf1odlem4  35138  erdszelem8  35230  erdszelem11  35233  erdsze2lem2  35236  connpconn  35267  sconnpi1  35271  cvmsss2  35306  cvmfolem  35311  cvmliftmolem2  35314  cvmliftlem15  35330  cvmlift2lem1  35334  cvmlift3lem4  35354  cvmlift3lem5  35355  satfdmlem  35400  fmla1  35419  gonarlem  35426  gonar  35427  goalrlem  35428  goalr  35429  fmla0disjsuc  35430  fmlasucdisj  35431  satffunlem1lem1  35434  satffunlem1lem2  35435  satffunlem2lem1  35436  mrsub0  35548  mrsubcn  35551  msubrn  35561  msubvrs  35592  br8  35788  br6  35789  br4  35790  cgrtriv  36035  btwntriv2  36045  btwncomim  36046  btwnswapid  36050  btwnintr  36052  btwnexch3  36053  btwnouttr2  36055  ifscgr  36077  cgrxfr  36088  btwnxfr  36089  btwnconn3  36136  segcon2  36138  brsegle  36141  seglecgr12im  36143  broutsideof3  36159  linethru  36186  elhf2  36208  opnregcld  36363  cldregopn  36364  neibastop2lem  36393  matunitlindflem1  37655  poimirlem16  37675  poimirlem17  37676  poimirlem19  37678  poimirlem20  37679  poimirlem24  37683  poimirlem29  37688  heicant  37694  opnmbllem0  37695  ismblfin  37700  itg2addnclem  37710  itg2addnclem3  37712  itg2gt0cn  37714  ftc1anclem5  37736  ftc2nc  37741  filbcmb  37779  fdc  37784  incsequz  37787  caushft  37800  istotbnd3  37810  equivbnd  37829  cntotbnd  37835  heibor1lem  37848  heibor1  37849  bfplem2  37862  divrngidl  38067  prnc  38106  lshpdisj  39025  cvrcon3b  39315  atnle  39355  hlhgt2  39427  hl0lt1N  39428  hl2at  39443  cvrexchlem  39457  cvratlem  39459  lvolnlelpln  39623  2lplnj  39658  ispsubcl2N  39985  lautcvr  40130  dva1dim  41023  dib1dim  41203  dib1dim2  41206  diclspsn  41232  dih1dimatlem  41367  dihlatat  41375  dihatexv  41376  dihatexv2  41377  lcfrlem9  41588  lcfrlem16  41596  mapdrvallem2  41683  mapd1o  41686  aks6d1c2  42162  elre0re  42286  prjspner1  42658  dffltz  42666  rexlimdv3d  42715  elrfi  42726  isnacs3  42742  eldiophb  42789  eldiophss  42806  diophren  42845  rencldnfilem  42852  pell1234qrdich  42893  pellfundex  42918  lsmfgcl  43106  kercvrlsm  43115  lmhmfgima  43116  lpirlnr  43149  hbtlem2  43156  hbtlem4  43158  hbtlem6  43161  rngunsnply  43201  onexoegt  43276  oaabsb  43326  cantnfresb  43356  omabs2  43364  tfsconcatrev  43380  restuni3  45154  limsupubuz  45750  stoweidlem57  46094  fourierdlem48  46191  fourierdlem49  46192  sge0le  46444  fsetsniunop  47079  cfsetsnfsetfo  47090  fcoresf1  47099  euoreqb  47139  modlt0b  47393  imasetpreimafvbijlemf1  47434  imasetpreimafvbijlemfo  47435  iccpartrn  47460  iccpartiun  47464  iccpartnel  47468  paireqne  47541  reupr  47552  odz2prm2pw  47593  fmtnofac2lem  47598  prmdvdsfmtnof1lem2  47615  2pwp1prm  47619  mod42tp1mod8  47632  lighneallem3  47637  lighneallem4  47640  requad01  47651  requad2  47653  fppr2odd  47761  gbowpos  47789  gbowgt5  47792  gboge9  47794  nnsum4primesodd  47826  nnsum4primesoddALTV  47827  isubgredg  47896  grimcnv  47918  uhgrimedgi  47920  isuspgrim0  47924  isuspgrimlem  47925  gricushgr  47947  clnbgrgrimlem  47963  clnbgrgrim  47964  grimedg  47965  grtrissvtx  47974  stgrusgra  47989  isubgr3stgrlem7  48002  gpgiedgdmellem  48076  gpgusgralem  48086  gpgvtxedg0  48093  gpgvtxedg1  48094  copisnmnd  48199  lidldomn1  48261  affinecomb1  48733  eenglngeehlnmlem2  48769  rrx2vlinest  48772  itsclquadb  48807  aacllem  49832