Theorem rexlimdva 3163

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-rex 3087

This theorem is used by:  rexlimdvaa  3164  rexlimivv  3204  rexlimdvv  3218  rspceb2dv  3580  ssexnelpss  4044  ralxfrd2  5373  iunopeqop  5493  iunopeqopOLD  5494  elsnxp  6294  foco2  7110  elunirn  7256  f1elima  7268  mptcnfimad  7999  releldmdifi  8057  mpoexw  8092  xpord3pred  8172  sexp3  8173  tfrlem9a  8398  seqomlem2  8465  oawordexr  8568  odi  8591  oelimcl  8613  nnawordex  8650  nnaordex  8651  oaabs  8661  oaabs2  8662  omabs  8664  eldifsucnn  8677  coflton  8684  cofon1  8685  cofon2  8686  cofonr  8687  naddunif  8707  ectocld  8807  onfin  9234  dif1ennnALT  9272  isfinite2  9294  isfiniteg  9296  fofinf1o  9325  elfiun  9426  suplub2  9457  supisoex  9471  ordtypelem9  9524  ordtypelem10  9525  brwdom2  9571  brwdom3  9580  ttrcltr  9721  rankr1ai  9810  elhf2  9914  fodomfi2  10143  infpwfien  10145  dfac12r  10229  ackbij1  10319  cff1  10340  fin23lem21  10421  isf32lem2  10436  fin1a2lem11  10492  fin1a2lem13  10494  ficard  10653  gchina  10788  eltsk2g  10840  tskhf  10857  rankcf  10866  inatsk  10867  tskuni  10872  nqereu  11018  ltexnq  11064  1idpr  11118  suplem1pr  11141  supsrlem  11200  axpre-sup  11258  1re  11312  0re  11314  0cnALT  11549  supaddc  12288  supadd  12289  supmul1  12290  supmul  12293  suprzcl2  13069  qmulz  13082  elpq  13107  qbtwnre  13333  ioo0  13505  ico0  13526  ioc0  13527  icc0  13528  addmodlteq  14093  fsequb  14122  hashdom  14527  ccats1alpha  14772  reuccatpfxs1lem  14900  shftlem  15227  rexuzre  15526  rexico  15527  caubnd  15532  limsupbnd1  15655  limsupbnd2  15656  rlim2lt  15670  rlim3  15671  lo1bdd2  15697  lo1bddrp  15698  o1lo1  15710  climuni  15725  climshftlem  15747  o1co  15759  rlimcn1  15761  climcn1  15765  o1rlimmul  15792  lo1le  15825  rlimno1  15827  isercoll  15841  caurcvg2  15851  serf0  15854  summolem2  15888  zsum  15890  fsum2dlem  15942  geomulcvg  16051  mertenslem2  16060  ntrivcvg  16072  zprod  16110  fprod2dlem  16153  dvds1lem  16443  dvdsexp2im  16503  odd2np1lem  16516  sqoddm1div8z  16530  ltoddhalfle  16537  halfleoddlt  16538  flodddiv4  16591  dvdssqim  16733  dvdsexpim  16734  coprmdvds2  16835  divgcdcoprm0  16846  cncongr1  16848  cncongr2  16849  isprm5  16889  rpexp  16904  pythagtriplem1  17000  iserodd  17019  pc2dvds  17063  difsqpwdvds  17071  oddprmdvds  17087  prmpwdvds  17088  4sqlem11  17139  vdwapun  17158  vdwlem2  17166  vdwlem6  17170  vdwlem8  17172  vdwlem10  17174  vdwnnlem1  17179  vdwnnlem3  17181  0ram  17204  ramub1lem2  17211  ramcl  17213  cshwsiun  17283  cshwrepswhash1  17286  firest  17609  imasvscafn  17715  imasmgm2  18869  imasmnd2  18974  dfgrp3lem  19254  imasgrp2  19271  issubg4  19362  cycsubm  19423  gaorber  19528  orbsta  19533  pmtr3ncom  19695  psgnran  19735  odmulg  19776  odbezout  19778  gexdvdsi  19803  sylow1lem3  19820  odcau  19824  sylow2alem1  19837  sylow3lem6  19852  lsmelvalm  19871  efgrelexlemb  19970  efgredeu  19972  imasabl  20096  cyggeninv  20103  cygctb  20112  cyggexb  20119  dprdssv  20238  dprddisj2  20261  ablfacrplem  20287  pgpfac1lem2  20297  pgpfac1lem5  20301  ringinvnzdiv  20538  imasring  20566  dvdsrcl2  20602  dvdsrmul1  20605  lss1d  21244  lssats2  21281  lspsn  21283  lmhmima  21328  rspsn0  21532  ring2idlqusb  21612  rngqiprngfulem2  21614  lpiss  21659  dvdsrzring  21773  pzriprnglem5  21797  pzriprnglem8  21800  pzriprnglem10  21802  pzriprnglem11  21803  znunit  21875  znrrg  21877  cygznlem3  21881  frgpcyg  21885  lindfrn  22133  mplcoe5lem  22354  mpfind  22430  gsummoncoe1  22632  mpfpf1  22675  pf1mpf  22676  mat1dimelbas  22792  scmatdmat  22836  scmataddcl  22837  scmatsubcl  22838  scmatmulcl  22839  matunitlindflem1  23000  cpmatacl  23040  chpscmat  23166  tgcl  23293  clsval2  23374  innei  23449  restcld  23496  restcldr  23498  ordtrest2lem  23527  cnprest  23613  lmss  23622  lmcls  23626  lmcnp  23628  isreg2  23701  cmpcovf  23715  cncmp  23716  cmpsub  23724  1stcrest  23777  2ndcrest  23778  1stccnp  23787  restnlly  23807  cldllycmp  23820  locfincmp  23851  txcnpi  23933  pthaus  23963  txtube  23965  txcmplem1  23966  txcmplem2  23967  txlm  23973  xkohaus  23978  xkococnlem  23984  xkococn  23985  kqfvima  24055  kqreglem1  24066  isfild  24183  filuni  24210  isufil2  24233  uffix  24246  rnelfm  24278  fmfnfmlem2  24280  fmfnfmlem4  24282  fmfnfm  24283  fmco  24286  fclsopn  24339  ufilcmp  24357  cnpfcf  24366  alexsublem  24369  alexsubALT  24376  cldsubg  24436  ghmcnp  24440  qustgpopn  24445  tsmsgsum  24464  tsmsres  24469  tsmsxplem1  24478  tsmsxp  24480  isucn2  24603  ucnprima  24606  imasdsf1olem  24698  blssps  24749  blss  24750  blssexps  24751  blssex  24752  mopni3  24819  blcld  24830  metrest  24849  metcnp3  24865  reperflem  25144  icccmplem3  25150  xrge0tsms  25160  mulc1cncf  25232  cncfco  25234  cnheibor  25282  bndth  25285  lebnumlem3  25290  xlebnum  25292  lebnumii  25293  nmhmcn  25447  cfil3i  25596  cmetcaulem  25615  cfilres  25623  bcthlem4  25654  ivthlem2  25779  ivthlem3  25780  ivthicc  25785  cniccbdd  25788  ovolunlem1  25824  ovoliunlem2  25830  ovolshftlem2  25837  ovolicc2  25849  iunmbl2  25884  dyadmax  25925  opnmbllem  25928  subopnmbl  25931  volivth  25934  ismbf3d  25981  mbfimaopn2  25984  mbfaddlem  25987  i1fmullem  26021  mbfi1fseqlem4  26045  bddiblnc  26168  ellimc3  26205  dvlip  26319  dvlip2  26321  c1liplem1  26322  dvgt0lem1  26328  dvivthlem2  26335  dvne0  26337  lhop1lem  26339  lhop2  26341  lhop  26342  tdeglem4  26384  mdegnn0cl  26395  ply1divex  26461  dvdsq1p  26487  ig1peu  26499  elply2  26520  plypf1  26537  plydivex  26624  aalioulem3  26667  aalioulem5  26669  aaliou  26671  ulmshftlem  26722  ulmcau  26728  ulmss  26730  ulmbdd  26731  ulmcn  26732  radcnvlt1  26751  eflogeq  26936  efopn  26992  cxpeq  27091  angpieqvd  27165  xrlimcnp  27302  cxploglim  27311  ftalem2  27407  ftalem7  27412  isppw2  27448  dchrptlem1  27597  dchrptlem3  27599  dchrsum2  27601  lgsdchrval  27687  lgsdchr  27688  gausslemma2dlem1a  27698  lgsquadlem1  27713  2lgsoddprmlem2  27742  dchrisumlem3  27824  dchrisum0fno1  27844  pntlem3  27942  pntleml  27944  ostth3  27971  fltoprm  28001  nosupno  28066  nosupbday  28068  noinfbday  28083  cutsun12  28182  oldssmade  28259  addsproplem2  28362  addsuniflem  28393  addbdaylem  28409  negsid  28433  negsunif  28447  negleft  28450  negright  28451  precsexlem6  28604  precsexlem7  28605  precsexlem11  28609  bdayons  28668  onaddscl  28669  om2noseqlt  28691  noseqrdgfn  28698  n0fincut  28747  bdayn0sf1o  28762  dfnns2  28764  bdaypw2n0bndlem  28855  bdayfinbndlem1  28859  z12negscl  28870  z12zsodd  28874  z12bdaylem  28876  bdayfinlem  28878  recut  28886  elreno2  28887  brcgr  29484  brbtwn2  29489  axbtwnid  29523  axcontlem7  29554  usgrnloopALT  29790  uhgrspansubgrlem  29877  nbuhgr  29930  nbupgr  29931  wwlksnextprop  30507  elwspths2on  30557  elwspths2onw  30558  erclwwlktr  30619  clwwlknscsh  30659  erclwwlkntr  30668  hashecclwwlkn1  30674  umgrhashecclwwlk  30675  3cyclfrgrrn1  30892  frgrregorufr  30932  frgr2wwlk1  30936  ubthlem1  31478  ubthlem3  31480  htthlem  31525  omlsii  32011  spansncol  32176  nmopun  32622  nmcexi  32634  riesz1  32673  elpjrn  32798  cvcon3  32892  chcv1  32963  atcvatlem  32993  chirredi  33002  br8d  33250  xrge0tsmsd  33681  ordtrest2NEWlem  34601  lmxrge0  34631  esumfsup  34749  esumpcvgval  34757  measdivcstALTV  34905  eulerpartlemgh  35057  dstfrvunirn  35154  afsval  35350  onvf1odlem4  35954  onprcf1acwevdlem1  35965  erdszelem8  36050  erdszelem11  36053  erdsze2lem2  36056  connpconn  36087  sconnpi1  36091  cvmsss2  36126  cvmfolem  36131  cvmliftmolem2  36134  cvmliftlem15  36150  cvmlift2lem1  36154  cvmlift3lem4  36174  cvmlift3lem5  36175  satfdmlem  36220  fmla1  36239  gonarlem  36246  gonar  36247  goalrlem  36248  goalr  36249  fmla0disjsuc  36250  fmlasucdisj  36251  satffunlem1lem1  36254  satffunlem1lem2  36255  satffunlem2lem1  36256  mrsub0  36368  mrsubcn  36371  msubrn  36381  msubvrs  36412  br8  36614  br6  36615  br4  36616  cgrtriv  36860  btwntriv2  36870  btwncomim  36871  btwnswapid  36875  btwnintr  36877  btwnexch3  36878  btwnouttr2  36880  ifscgr  36902  cgrxfr  36913  btwnxfr  36914  btwnconn3  36961  segcon2  36963  brsegle  36966  seglecgr12im  36968  broutsideof3  36984  linethru  37011  nmulprop  37032  opnregcld  37211  cldregopn  37212  neibastop2lem  37241  tr0elw  37365  tr0el  37366  poimirlem16  38648  poimirlem17  38649  poimirlem19  38651  poimirlem20  38652  poimirlem24  38656  poimirlem29  38661  heicant  38667  opnmbllem0  38668  ismblfin  38673  itg2addnclem  38683  itg2addnclem3  38685  itg2gt0cn  38687  ftc1anclem5  38709  ftc2nc  38714  filbcmb  38768  fdc  38773  incsequz  38776  caushft  38789  istotbnd3  38799  equivbnd  38818  cntotbnd  38824  heibor1lem  38837  heibor1  38838  bfplem2  38851  divrngidl  39056  prnc  39095  lshpdisj  40138  cvrcon3b  40428  atnle  40468  hlhgt2  40540  hl0lt1N  40541  hl2at  40556  cvrexchlem  40570  cvratlem  40572  lvolnlelpln  40736  2lplnj  40771  ispsubcl2N  41098  lautcvr  41243  dva1dim  42136  dib1dim  42316  dib1dim2  42319  diclspsn  42345  dih1dimatlem  42480  dihlatat  42488  dihatexv  42489  dihatexv2  42490  lcfrlem9  42701  lcfrlem16  42709  mapdrvallem2  42796  mapd1o  42799  aks6d1c2  43274  elre0re  43399  dffltz  43764  rexlimdv3d  43787  elrfi  43799  isnacs3  43815  eldiophb  43862  eldiophss  43879  diophren  43914  rencldnfilem  43921  pell1234qrdich  43962  pellfundex  43987  lsmfgcl  44170  kercvrlsm  44179  lmhmfgima  44180  lpirlnr  44213  hbtlem2  44220  hbtlem4  44222  hbtlem6  44225  rngunsnply  44265  onexoegt  44340  oaabsb  44390  cantnfresb  44420  omabs2  44428  tfsconcatrev  44444  restuni3  46227  limsupubuz  46817  stoweidlem57  47161  fourierdlem48  47258  fourierdlem49  47259  sge0le  47511  fsetsniunop  48213  cfsetsnfsetfo  48224  fcoresf1  48233  euoreqb  48273  modlt0b  48533  nndivides2  48548  imasetpreimafvbijlemf1  48580  imasetpreimafvbijlemfo  48581  iccpartrn  48606  iccpartiun  48610  iccpartnel  48614  paireqne  48687  reupr  48698  odz2prm2pw  48742  fmtnofac2lem  48747  prmdvdsfmtnof1lem2  48764  2pwp1prm  48768  mod42tp1mod8  48781  lighneallem3  48786  lighneallem4  48789  nprmdvdsfacm1  48803  ppivalnnprm  48804  ppivalnnnprmge6  48805  requad01  48813  requad2  48815  fppr2odd  48923  gbowpos  48951  gbowgt5  48954  gboge9  48956  nnsum4primesodd  48988  nnsum4primesoddALTV  48989  isubgredg  49058  grimcnv  49080  uhgrimedgi  49082  isuspgrim0  49086  isuspgrimlem  49087  gricushgr  49109  clnbgrgrimlem  49125  clnbgrgrim  49126  grimedg  49127  grtrissvtx  49136  stgrusgra  49151  isubgr3stgrlem7  49164  gpgiedgdmellem  49238  gpgusgralem  49248  gpgvtxedg0  49255  gpgvtxedg1  49256  copisnmnd  49360  lidldomn1  49422  affinecomb1  49908  eenglngeehlnmlem2  49945  itsclquadb  49982  aacllem  51108