Theorem rexlimdvaa 3153

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-rex 3068

This theorem is referenced by:  rexlimddv  3158  tz7.7  6411  isofrlem  7359  nnawordex  8673  nnaordex2  8675  oaabs2  8685  fiin  9459  marypha1lem  9470  wemaplem3  9585  cantnflt  9709  fseqenlem2  10062  cardaleph  10126  coftr  10310  fin23lem26  10362  fin1a2lem13  10449  fpwwe2  10680  r1wunlim  10774  wunex2  10775  inttsk  10811  grur1  10857  inaprc  10873  receu  11905  zsupss  12976  xralrple  13243  rexanuz  15380  limsupval2  15512  caucvgb  15712  fsumiun  15853  rpnnen2lem12  16257  dvdsval2  16289  prmind2  16718  prmdvdsncoprmbd  16760  pcprmpw2  16915  pockthg  16939  prmreclem5  16953  vdwlem6  17019  vdwlem10  17023  sscpwex  17862  drsdirfi  18362  psgnunilem3  19528  sylow3lem2  19660  efgsfo  19771  lt6abl  19927  ghmcyg  19928  ablsimpgfind  20144  unitgrp  20399  irredrmul  20443  drngnidl  21270  znunit  21599  tgcl  22991  neiint  23127  restopnb  23198  ordtrest2lem  23226  pnfnei  23243  mnfnei  23244  iscnp4  23286  haust1  23375  ordthauslem  23406  tgcmp  23424  t1connperf  23459  2ndc1stc  23474  2ndcdisj  23479  islly2  23507  nllyrest  23509  reftr  23537  comppfsc  23555  ptbasfi  23604  ptcnp  23645  xkococnlem  23682  tgqtop  23735  fbssfi  23860  fgabs  23902  neifil  23903  trfil2  23910  elfm2  23971  elfm3  23973  rnelfmlem  23975  fmfnfmlem4  23980  flffbas  24018  fclsfnflim  24050  ptcmplem4  24078  tsmsxp  24178  blssexps  24451  blssex  24452  icccmplem3  24859  cnheibor  25000  pi1blem  25085  iscfil3  25320  iscmet3lem2  25339  metsscmetcld  25362  ovolicc2  25570  nulmbl2  25584  volsup  25604  dyadmbllem  25647  itg2const2  25790  bddmulibl  25888  bddiblnc  25891  limcflf  25930  itgsubst  26104  ulmdvlem3  26459  xrlimcnp  27025  amgm  27048  dchrptlem2  27323  lgsne0  27393  lgsqr  27409  lgsquadlem1  27438  dchrvmasumif  27561  rpvmasum2  27570  dchrisum0re  27571  dchrisum0lem3  27577  dchrisum0  27578  dchrmusum  27582  dchrvmasum  27583  chpdifbnd  27613  pntrlog2bnd  27642  pntibndlem3  27650  pntibnd  27651  pntleml  27669  ostth  27697  nosupno  27762  nosupbnd1lem1  27767  nosupbnd2  27775  noinfno  27777  noinfbnd1lem1  27782  noinfbnd2  27790  scutbdaybnd2  27875  oldlim  27939  oldbdayim  27941  sleadd1  28036  norecdiv  28230  precsexlem11  28255  noseqrdgfn  28326  brbtwn2  28934  colinearalg  28939  nbumgrvtx  29377  cusgrfilem1  29487  nmobndi  30803  spansneleq  31598  ofrn2  32656  xreceu  32888  ordtrest2NEWlem  33882  dya2iocnei  34263  connpconn  35219  cvmsss2  35258  cvmlift2lem10  35296  cvmlift3lem2  35304  outsidele  36113  neibastop1  36341  neibastop2lem  36342  matunitlindflem1  37602  mblfinlem1  37643  mblfinlem3  37645  mblfinlem4  37646  ismblfin  37647  cnambfre  37654  itg2addnclem  37657  itg2addnclem3  37659  ftc1anclem7  37685  ftc1anc  37687  fdc  37731  sstotbnd2  37760  sstotbnd  37761  isbndx  37768  ssbnd  37774  totbndbnd  37775  heibor  37807  unichnidl  38017  pexmidlem8N  39959  sn-0tie0  42445  nna4b4nsq  42646  elrfi  42681  fnwe2lem2  43039  hbtlem5  43116  rexlimdvaacbv  44194  rexlimddvcbvw  44195  liminfval2  45723  2zrngamgm  48088