Theorem rexlimdvaa 3157

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 458	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
3	2	rexlimdva 3156	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  ∃wrex 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3072

This theorem is referenced by:  rexlimddv  3162  tz7.7  6391  isofrlem  7337  nnawordex  8637  oaabs2  8648  fiin  9417  marypha1lem  9428  wemaplem3  9543  cantnflt  9667  fseqenlem2  10020  cardaleph  10084  coftr  10268  fin23lem26  10320  fin1a2lem13  10407  fpwwe2  10638  r1wunlim  10732  wunex2  10733  inttsk  10769  grur1  10815  inaprc  10831  receu  11859  zsupss  12921  xralrple  13184  rexanuz  15292  limsupval2  15424  caucvgb  15626  fsumiun  15767  rpnnen2lem12  16168  dvdsval2  16200  prmind2  16622  prmdvdsncoprmbd  16663  pcprmpw2  16815  pockthg  16839  prmreclem5  16853  vdwlem6  16919  vdwlem10  16923  sscpwex  17762  drsdirfi  18258  psgnunilem3  19364  sylow3lem2  19496  efgsfo  19607  lt6abl  19763  ghmcyg  19764  ablsimpgfind  19980  unitgrp  20197  irredrmul  20241  drngnidl  20854  znunit  21119  tgcl  22472  neiint  22608  restopnb  22679  ordtrest2lem  22707  pnfnei  22724  mnfnei  22725  iscnp4  22767  haust1  22856  ordthauslem  22887  tgcmp  22905  t1connperf  22940  2ndc1stc  22955  2ndcdisj  22960  islly2  22988  nllyrest  22990  reftr  23018  comppfsc  23036  ptbasfi  23085  ptcnp  23126  xkococnlem  23163  tgqtop  23216  fbssfi  23341  fgabs  23383  neifil  23384  trfil2  23391  elfm2  23452  elfm3  23454  rnelfmlem  23456  fmfnfmlem4  23461  flffbas  23499  fclsfnflim  23531  ptcmplem4  23559  tsmsxp  23659  blssexps  23932  blssex  23933  icccmplem3  24340  cnheibor  24471  pi1blem  24555  iscfil3  24790  iscmet3lem2  24809  metsscmetcld  24832  ovolicc2  25039  nulmbl2  25053  volsup  25073  dyadmbllem  25116  itg2const2  25259  bddmulibl  25356  bddiblnc  25359  limcflf  25398  itgsubst  25566  ulmdvlem3  25914  xrlimcnp  26473  amgm  26495  dchrptlem2  26768  lgsne0  26838  lgsqr  26854  lgsquadlem1  26883  dchrvmasumif  27006  rpvmasum2  27015  dchrisum0re  27016  dchrisum0lem3  27022  dchrisum0  27023  dchrmusum  27027  dchrvmasum  27028  chpdifbnd  27058  pntrlog2bnd  27087  pntibndlem3  27095  pntibnd  27096  pntleml  27114  ostth  27142  nosupno  27206  nosupbnd1lem1  27211  nosupbnd2  27219  noinfno  27221  noinfbnd1lem1  27226  noinfbnd2  27234  scutbdaybnd2  27317  oldlim  27381  oldbdayim  27383  sleadd1  27472  norecdiv  27638  precsexlem11  27663  brbtwn2  28163  colinearalg  28168  nbumgrvtx  28603  cusgrfilem1  28712  nmobndi  30028  spansneleq  30823  ofrn2  31865  xreceu  32088  ordtrest2NEWlem  32902  dya2iocnei  33281  connpconn  34226  cvmsss2  34265  cvmlift2lem10  34303  cvmlift3lem2  34311  outsidele  35104  neibastop1  35244  neibastop2lem  35245  matunitlindflem1  36484  mblfinlem1  36525  mblfinlem3  36527  mblfinlem4  36528  ismblfin  36529  cnambfre  36536  itg2addnclem  36539  itg2addnclem3  36541  ftc1anclem7  36567  ftc1anc  36569  fdc  36613  sstotbnd2  36642  sstotbnd  36643  isbndx  36650  ssbnd  36656  totbndbnd  36657  heibor  36689  unichnidl  36899  pexmidlem8N  38848  sn-0tie0  41312  nna4b4nsq  41402  elrfi  41432  fnwe2lem2  41793  hbtlem5  41870  rexlimdvaacbv  42957  rexlimddvcbvw  42958  liminfval2  44484  2zrngamgm  46837