Theorem rexlimdva 3196

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2110  ∃wrex 3055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-ral 3059  df-rex 3060

This theorem is referenced by:  rexlimdvaa  3197  rexlimivv  3204  rexlimdvv  3205  ssexnelpss  4018  ralxfrd2  5294  iunopeqop  5393  elsnxp  6143  foco2  6915  elunirn  7053  f1elima  7064  releldmdifi  7805  mpoexw  7838  tfrlem9a  8111  seqomlem2  8176  oawordexr  8273  odi  8296  oelimcl  8317  nnawordex  8354  nnaordex  8355  oaabs  8362  oaabs2  8363  omabs  8365  ectocld  8455  onfin  8859  dif1enALT  8896  isfinite2  8918  isfiniteg  8920  fofinf1o  8940  elfiun  9035  suplub2  9066  supisoex  9079  ordtypelem9  9131  ordtypelem10  9132  brwdom2  9178  brwdom3  9187  rankr1ai  9397  fodomfi2  9657  infpwfien  9659  dfac12r  9743  ackbij1  9835  cff1  9855  fin23lem21  9936  isf32lem2  9951  fin1a2lem11  10007  fin1a2lem13  10009  ficard  10162  gchina  10296  eltsk2g  10348  tskr1om2  10365  rankcf  10374  inatsk  10375  tskuni  10380  nqereu  10526  ltexnq  10572  1idpr  10626  suplem1pr  10649  supsrlem  10708  axpre-sup  10766  1re  10816  0re  10818  0cnALT  11049  negfi  11764  supaddc  11782  supadd  11783  supmul1  11784  supmul  11787  suprzcl2  12517  qmulz  12530  elpq  12554  qbtwnre  12772  ioo0  12943  ico0  12964  ioc0  12965  icc0  12966  addmodlteq  13502  fsequb  13531  hashdom  13929  ccats1alpha  14159  reuccatpfxs1lem  14294  shftlem  14614  rexuzre  14899  rexico  14900  caubnd  14905  limsupbnd1  15026  limsupbnd2  15027  rlim2lt  15041  rlim3  15042  lo1bdd2  15068  lo1bddrp  15069  o1lo1  15081  climuni  15096  climshftlem  15118  o1co  15130  rlimcn1  15132  climcn1  15136  o1rlimmul  15163  lo1le  15198  rlimno1  15200  isercoll  15214  caurcvg2  15224  serf0  15227  summolem2  15263  zsum  15265  fsum2dlem  15315  geomulcvg  15421  mertenslem2  15430  ntrivcvg  15442  zprod  15480  fprod2dlem  15523  dvds1lem  15810  dvdsexp2im  15869  odd2np1lem  15882  sqoddm1div8z  15896  ltoddhalfle  15903  halfleoddlt  15904  flodddiv4  15955  dvdssqim  16097  coprmdvds2  16192  divgcdcoprm0  16203  cncongr1  16205  cncongr2  16206  isprm5  16245  rpexp  16260  pythagtriplem1  16350  iserodd  16369  pc2dvds  16413  difsqpwdvds  16421  oddprmdvds  16437  prmpwdvds  16438  4sqlem11  16489  vdwapun  16508  vdwlem2  16516  vdwlem6  16520  vdwlem8  16522  vdwlem10  16524  vdwnnlem1  16529  vdwnnlem3  16531  0ram  16554  ramub1lem2  16561  ramcl  16563  cshwsiun  16634  cshwrepswhash1  16637  firest  16909  imasvscafn  17014  imasmnd2  18182  dfgrp3lem  18433  imasgrp2  18450  issubg4  18534  cycsubm  18581  gaorber  18674  orbsta  18679  pmtr3ncom  18839  psgnran  18879  odmulg  18919  odbezout  18921  gexdvdsi  18944  sylow1lem3  18961  odcau  18965  sylow2alem1  18978  sylow3lem6  18993  lsmelvalm  19012  efgrelexlemb  19112  efgredeu  19114  cyggeninv  19239  cygctb  19249  cyggexb  19256  dprdssv  19375  dprddisj2  19398  ablfacrplem  19424  pgpfac1lem2  19434  pgpfac1lem5  19438  ringinvnzdiv  19583  imasring  19609  dvdsrcl2  19640  dvdsrmul1  19643  lss1d  19972  lssats2  20009  lspsn  20011  lmhmima  20056  lpiss  20260  dvdsrzring  20420  znunit  20500  znrrg  20502  cygznlem3  20506  frgpcyg  20510  lindfrn  20755  mplcoe5lem  20968  mpfind  21039  gsummoncoe1  21197  mpfpf1  21239  pf1mpf  21240  mat1dimelbas  21340  scmatdmat  21384  scmataddcl  21385  scmatsubcl  21386  scmatmulcl  21387  cpmatacl  21585  chpscmat  21711  tgcl  21838  clsval2  21919  innei  21994  restcld  22041  restcldr  22043  ordtrest2lem  22072  cnprest  22158  lmss  22167  lmcls  22171  lmcnp  22173  isreg2  22246  cmpcovf  22260  cncmp  22261  cmpsub  22269  1stcrest  22322  2ndcrest  22323  1stccnp  22331  restnlly  22351  cldllycmp  22364  locfincmp  22395  txcnpi  22477  pthaus  22507  txtube  22509  txcmplem1  22510  txcmplem2  22511  txlm  22517  xkohaus  22522  xkococnlem  22528  xkococn  22529  kqfvima  22599  kqreglem1  22610  isfild  22727  filuni  22754  isufil2  22777  uffix  22790  rnelfm  22822  fmfnfmlem2  22824  fmfnfmlem4  22826  fmfnfm  22827  fmco  22830  fclsopn  22883  ufilcmp  22901  cnpfcf  22910  alexsublem  22913  alexsubALT  22920  cldsubg  22980  ghmcnp  22984  qustgpopn  22989  tsmsgsum  23008  tsmsres  23013  tsmsxplem1  23022  tsmsxp  23024  isucn2  23148  ucnprima  23151  imasdsf1olem  23243  blssps  23294  blss  23295  blssexps  23296  blssex  23297  mopni3  23364  blcld  23375  metrest  23394  metcnp3  23410  reperflem  23687  icccmplem3  23693  xrge0tsms  23703  mulc1cncf  23774  cncfco  23776  cnheibor  23824  bndth  23827  lebnumlem3  23832  xlebnum  23834  lebnumii  23835  nmhmcn  23989  cfil3i  24138  cmetcaulem  24157  cfilres  24165  bcthlem4  24196  ivthlem2  24321  ivthlem3  24322  ivthicc  24327  cniccbdd  24330  ovolunlem1  24366  ovoliunlem2  24372  ovolshftlem2  24379  ovolicc2  24391  iunmbl2  24426  dyadmax  24467  opnmbllem  24470  subopnmbl  24473  volivth  24476  ismbf3d  24523  mbfimaopn2  24526  mbfaddlem  24529  i1fmullem  24563  mbfi1fseqlem4  24588  bddiblnc  24711  ellimc3  24748  dvlip  24862  dvlip2  24864  c1liplem1  24865  dvgt0lem1  24871  dvivthlem2  24878  dvne0  24880  lhop1lem  24882  lhop2  24884  lhop  24885  tdeglem4  24929  tdeglem4OLD  24930  mdegnn0cl  24941  ply1divex  25006  dvdsq1p  25030  ig1peu  25041  elply2  25062  plypf1  25078  plydivex  25162  aalioulem3  25199  aalioulem5  25201  aaliou  25203  ulmshftlem  25253  ulmcau  25259  ulmss  25261  ulmbdd  25262  ulmcn  25263  radcnvlt1  25282  eflogeq  25462  efopn  25518  cxpeq  25615  angpieqvd  25686  xrlimcnp  25823  cxploglim  25832  ftalem2  25928  ftalem7  25933  isppw2  25969  dchrptlem1  26117  dchrptlem3  26119  dchrsum2  26121  lgsdchrval  26207  lgsdchr  26208  gausslemma2dlem1a  26218  lgsquadlem1  26233  2lgsoddprmlem2  26262  dchrisumlem3  26344  dchrisum0fno1  26364  pntlem3  26462  pntleml  26464  ostth3  26491  brcgr  26963  brbtwn2  26968  axbtwnid  27002  axcontlem7  27033  usgrnloopALT  27263  uhgrspansubgrlem  27350  nbuhgr  27403  nbupgr  27404  wwlksnextprop  27968  elwspths2on  28016  erclwwlktr  28077  clwwlknscsh  28117  erclwwlkntr  28126  hashecclwwlkn1  28132  umgrhashecclwwlk  28133  3cyclfrgrrn1  28340  frgrregorufr  28380  frgr2wwlk1  28384  ubthlem1  28923  ubthlem3  28925  htthlem  28970  omlsii  29456  spansncol  29621  nmopun  30067  nmcexi  30079  riesz1  30118  elpjrn  30243  cvcon3  30337  chcv1  30408  atcvatlem  30438  chirredi  30447  br8d  30641  xrge0tsmsd  31008  ordtrest2NEWlem  31558  lmxrge0  31588  esumfsup  31722  esumpcvgval  31730  measdivcstALTV  31877  eulerpartlemgh  32029  dstfrvunirn  32125  afsval  32335  erdszelem8  32845  erdszelem11  32848  erdsze2lem2  32851  connpconn  32882  sconnpi1  32886  cvmsss2  32921  cvmfolem  32926  cvmliftmolem2  32929  cvmliftlem15  32945  cvmlift2lem1  32949  cvmlift3lem4  32969  cvmlift3lem5  32970  satfdmlem  33015  fmla1  33034  gonarlem  33041  gonar  33042  goalrlem  33043  goalr  33044  fmla0disjsuc  33045  fmlasucdisj  33046  satffunlem1lem1  33049  satffunlem1lem2  33050  satffunlem2lem1  33051  mrsub0  33163  mrsubcn  33166  msubrn  33176  msubvrs  33207  br8  33411  br6  33412  br4  33413  xpord3pred  33486  sexp3  33487  nosupno  33600  nosupbday  33602  noinfbday  33617  scutun12  33698  oldssmade  33754  cgrtriv  33998  btwntriv2  34008  btwncomim  34009  btwnswapid  34013  btwnintr  34015  btwnexch3  34016  btwnouttr2  34018  ifscgr  34040  cgrxfr  34051  btwnxfr  34052  btwnconn3  34099  segcon2  34101  brsegle  34104  seglecgr12im  34106  broutsideof3  34122  linethru  34149  elhf2  34171  opnregcld  34213  cldregopn  34214  neibastop2lem  34243  matunitlindflem1  35467  poimirlem16  35487  poimirlem17  35488  poimirlem19  35490  poimirlem20  35491  poimirlem24  35495  poimirlem29  35500  heicant  35506  opnmbllem0  35507  ismblfin  35512  itg2addnclem  35522  itg2addnclem3  35524  itg2gt0cn  35526  ftc1anclem5  35548  ftc2nc  35553  filbcmb  35592  fdc  35597  incsequz  35600  caushft  35613  istotbnd3  35623  equivbnd  35642  cntotbnd  35648  heibor1lem  35661  heibor1  35662  bfplem2  35675  divrngidl  35880  prnc  35919  lshpdisj  36695  cvrcon3b  36985  atnle  37025  hlhgt2  37097  hl0lt1N  37098  hl2at  37113  cvrexchlem  37127  cvratlem  37129  lvolnlelpln  37293  2lplnj  37328  ispsubcl2N  37655  lautcvr  37800  dva1dim  38693  dib1dim  38873  dib1dim2  38876  diclspsn  38902  dih1dimatlem  39037  dihlatat  39045  dihatexv  39046  dihatexv2  39047  lcfrlem9  39258  lcfrlem16  39266  mapdrvallem2  39353  mapd1o  39356  elre0re  39950  dvdsexpim  39988  prjspner1  40123  dffltz  40126  rexlimdv3d  40160  elrfi  40171  isnacs3  40187  eldiophb  40234  eldiophss  40251  diophren  40290  rencldnfilem  40297  pell1234qrdich  40338  pellfundex  40363  lsmfgcl  40554  kercvrlsm  40563  lmhmfgima  40564  lpirlnr  40597  hbtlem2  40604  hbtlem4  40606  hbtlem6  40609  rngunsnply  40653  restuni3  42292  limsupubuz  42883  stoweidlem57  43227  fourierdlem48  43324  fourierdlem49  43325  sge0le  43574  fsetsniunop  44169  cfsetsnfsetfo  44180  fcoresf1  44189  euoreqb  44227  imasetpreimafvbijlemf1  44483  imasetpreimafvbijlemfo  44484  iccpartrn  44509  iccpartiun  44513  iccpartnel  44517  paireqne  44590  reupr  44601  odz2prm2pw  44642  fmtnofac2lem  44647  prmdvdsfmtnof1lem2  44664  2pwp1prm  44668  mod42tp1mod8  44681  lighneallem3  44686  lighneallem4  44689  requad01  44700  requad2  44702  fppr2odd  44810  gbowpos  44838  gbowgt5  44841  gboge9  44843  nnsum4primesodd  44875  nnsum4primesoddALTV  44876  isomushgr  44905  isomuspgrlem2d  44910  copisnmnd  44990  lidldomn1  45106  affinecomb1  45675  eenglngeehlnmlem2  45711  rrx2vlinest  45714  itsclquadb  45749  rspceb2dv  45775  aacllem  46130