Theorem rexlimdvaa 3136

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Mario Carneiro, 15-Jun-2016.)

Hypothesis

Ref	Expression
rexlimdvaa.1	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒)

Assertion

Ref	Expression
rexlimdvaa	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Distinct variable groups:   𝜑,𝑥   𝜒,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimdvaa

Step	Hyp	Ref	Expression
1		rexlimdvaa.1	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒)
2	1	expr 456	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
3	2	rexlimdva 3135	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∃wrex 3054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3055

This theorem is referenced by:  rexlimddv  3141  tz7.7  6361  isofrlem  7318  nnawordex  8604  nnaordex2  8606  oaabs2  8616  fiin  9380  marypha1lem  9391  wemaplem3  9508  cantnflt  9632  fseqenlem2  9985  cardaleph  10049  coftr  10233  fin23lem26  10285  fin1a2lem13  10372  fpwwe2  10603  r1wunlim  10697  wunex2  10698  inttsk  10734  grur1  10780  inaprc  10796  receu  11830  zsupss  12903  xralrple  13172  rexanuz  15319  limsupval2  15453  caucvgb  15653  fsumiun  15794  rpnnen2lem12  16200  dvdsval2  16232  prmind2  16662  prmdvdsncoprmbd  16704  pcprmpw2  16860  pockthg  16884  prmreclem5  16898  vdwlem6  16964  vdwlem10  16968  sscpwex  17784  drsdirfi  18273  psgnunilem3  19433  sylow3lem2  19565  efgsfo  19676  lt6abl  19832  ghmcyg  19833  ablsimpgfind  20049  unitgrp  20299  irredrmul  20343  drngnidl  21160  znunit  21480  tgcl  22863  neiint  22998  restopnb  23069  ordtrest2lem  23097  pnfnei  23114  mnfnei  23115  iscnp4  23157  haust1  23246  ordthauslem  23277  tgcmp  23295  t1connperf  23330  2ndc1stc  23345  2ndcdisj  23350  islly2  23378  nllyrest  23380  reftr  23408  comppfsc  23426  ptbasfi  23475  ptcnp  23516  xkococnlem  23553  tgqtop  23606  fbssfi  23731  fgabs  23773  neifil  23774  trfil2  23781  elfm2  23842  elfm3  23844  rnelfmlem  23846  fmfnfmlem4  23851  flffbas  23889  fclsfnflim  23921  ptcmplem4  23949  tsmsxp  24049  blssexps  24321  blssex  24322  icccmplem3  24720  cnheibor  24861  pi1blem  24946  iscfil3  25180  iscmet3lem2  25199  metsscmetcld  25222  ovolicc2  25430  nulmbl2  25444  volsup  25464  dyadmbllem  25507  itg2const2  25649  bddmulibl  25747  bddiblnc  25750  limcflf  25789  itgsubst  25963  ulmdvlem3  26318  xrlimcnp  26885  amgm  26908  dchrptlem2  27183  lgsne0  27253  lgsqr  27269  lgsquadlem1  27298  dchrvmasumif  27421  rpvmasum2  27430  dchrisum0re  27431  dchrisum0lem3  27437  dchrisum0  27438  dchrmusum  27442  dchrvmasum  27443  chpdifbnd  27473  pntrlog2bnd  27502  pntibndlem3  27510  pntibnd  27511  pntleml  27529  ostth  27557  nosupno  27622  nosupbnd1lem1  27627  nosupbnd2  27635  noinfno  27637  noinfbnd1lem1  27642  noinfbnd2  27650  scutbdaybnd2  27735  oldlim  27805  oldbdayim  27807  sleadd1  27903  norecdiv  28100  precsexlem11  28126  noseqrdgfn  28207  pw2recs  28330  zs12ge0  28349  brbtwn2  28839  colinearalg  28844  nbumgrvtx  29280  cusgrfilem1  29390  nmobndi  30711  spansneleq  31506  ofrn2  32571  xreceu  32849  ordtrest2NEWlem  33919  dya2iocnei  34280  connpconn  35229  cvmsss2  35268  cvmlift2lem10  35306  cvmlift3lem2  35314  outsidele  36127  neibastop1  36354  neibastop2lem  36355  matunitlindflem1  37617  mblfinlem1  37658  mblfinlem3  37660  mblfinlem4  37661  ismblfin  37662  cnambfre  37669  itg2addnclem  37672  itg2addnclem3  37674  ftc1anclem7  37700  ftc1anc  37702  fdc  37746  sstotbnd2  37775  sstotbnd  37776  isbndx  37783  ssbnd  37789  totbndbnd  37790  heibor  37822  unichnidl  38032  pexmidlem8N  39978  sn-0tie0  42446  nna4b4nsq  42655  elrfi  42689  fnwe2lem2  43047  hbtlem5  43124  rexlimdvaacbv  44201  rexlimddvcbvw  44202  relpfrlem  44950  liminfval2  45773  2zrngamgm  48237