Theorem rexlimdvaa 3140

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  rexlimddv  3145  tz7.7  6351  isofrlem  7296  nnawordex  8575  nnaordex2  8577  oaabs2  8587  fiin  9337  marypha1lem  9348  wemaplem3  9465  cantnflt  9593  fseqenlem2  9947  cardaleph  10011  coftr  10195  fin23lem26  10247  fin1a2lem13  10334  fpwwe2  10566  r1wunlim  10660  wunex2  10661  inttsk  10697  grur1  10743  inaprc  10759  receu  11794  zsupss  12862  xralrple  13132  rexanuz  15281  limsupval2  15415  caucvgb  15615  fsumiun  15756  rpnnen2lem12  16162  dvdsval2  16194  prmind2  16624  prmdvdsncoprmbd  16666  pcprmpw2  16822  pockthg  16846  prmreclem5  16860  vdwlem6  16926  vdwlem10  16930  sscpwex  17751  drsdirfi  18240  psgnunilem3  19437  sylow3lem2  19569  efgsfo  19680  lt6abl  19836  ghmcyg  19837  ablsimpgfind  20053  unitgrp  20331  irredrmul  20375  drngnidl  21210  znunit  21530  tgcl  22925  neiint  23060  restopnb  23131  ordtrest2lem  23159  pnfnei  23176  mnfnei  23177  iscnp4  23219  haust1  23308  ordthauslem  23339  tgcmp  23357  t1connperf  23392  2ndc1stc  23407  2ndcdisj  23412  islly2  23440  nllyrest  23442  reftr  23470  comppfsc  23488  ptbasfi  23537  ptcnp  23578  xkococnlem  23615  tgqtop  23668  fbssfi  23793  fgabs  23835  neifil  23836  trfil2  23843  elfm2  23904  elfm3  23906  rnelfmlem  23908  fmfnfmlem4  23913  flffbas  23951  fclsfnflim  23983  ptcmplem4  24011  tsmsxp  24111  blssexps  24382  blssex  24383  icccmplem3  24781  cnheibor  24922  pi1blem  25007  iscfil3  25241  iscmet3lem2  25260  metsscmetcld  25283  ovolicc2  25491  nulmbl2  25505  volsup  25525  dyadmbllem  25568  itg2const2  25710  bddmulibl  25808  bddiblnc  25811  limcflf  25850  itgsubst  26024  ulmdvlem3  26379  xrlimcnp  26946  amgm  26969  dchrptlem2  27244  lgsne0  27314  lgsqr  27330  lgsquadlem1  27359  dchrvmasumif  27482  rpvmasum2  27491  dchrisum0re  27492  dchrisum0lem3  27498  dchrisum0  27499  dchrmusum  27503  dchrvmasum  27504  chpdifbnd  27534  pntrlog2bnd  27563  pntibndlem3  27571  pntibnd  27572  pntleml  27590  ostth  27618  nosupno  27683  nosupbnd1lem1  27688  nosupbnd2  27696  noinfno  27698  noinfbnd1lem1  27703  noinfbnd2  27711  cutbdaybnd2  27804  oldlim  27895  oldbdayim  27897  leadds1  27997  norecdiv  28198  precsexlem11  28225  noseqrdgfn  28314  pw2recs  28446  z12sge0  28491  brbtwn2  28990  colinearalg  28995  nbumgrvtx  29431  cusgrfilem1  29541  nmobndi  30862  spansneleq  31657  ofrn2  32729  xreceu  33013  ordtrest2NEWlem  34099  dya2iocnei  34459  connpconn  35448  cvmsss2  35487  cvmlift2lem10  35525  cvmlift3lem2  35533  outsidele  36345  neibastop1  36572  neibastop2lem  36573  matunitlindflem1  37864  mblfinlem1  37905  mblfinlem3  37907  mblfinlem4  37908  ismblfin  37909  cnambfre  37916  itg2addnclem  37919  itg2addnclem3  37921  ftc1anclem7  37947  ftc1anc  37949  fdc  37993  sstotbnd2  38022  sstotbnd  38023  isbndx  38030  ssbnd  38036  totbndbnd  38037  heibor  38069  unichnidl  38279  pexmidlem8N  40350  sn-0tie0  42818  nna4b4nsq  43015  elrfi  43048  fnwe2lem2  43405  hbtlem5  43482  rexlimdvaacbv  44558  rexlimddvcbvw  44559  relpfrlem  45306  liminfval2  46123  2zrngamgm  48602