Theorem rexlimdvaa 3143

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2107  ∃wrex 3059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-rex 3060

This theorem is referenced by:  rexlimddv  3148  tz7.7  6389  isofrlem  7342  nnawordex  8657  nnaordex2  8659  oaabs2  8669  fiin  9444  marypha1lem  9455  wemaplem3  9570  cantnflt  9694  fseqenlem2  10047  cardaleph  10111  coftr  10295  fin23lem26  10347  fin1a2lem13  10434  fpwwe2  10665  r1wunlim  10759  wunex2  10760  inttsk  10796  grur1  10842  inaprc  10858  receu  11890  zsupss  12961  xralrple  13229  rexanuz  15367  limsupval2  15499  caucvgb  15699  fsumiun  15840  rpnnen2lem12  16244  dvdsval2  16276  prmind2  16705  prmdvdsncoprmbd  16747  pcprmpw2  16903  pockthg  16927  prmreclem5  16941  vdwlem6  17007  vdwlem10  17011  sscpwex  17831  drsdirfi  18322  psgnunilem3  19483  sylow3lem2  19615  efgsfo  19726  lt6abl  19882  ghmcyg  19883  ablsimpgfind  20099  unitgrp  20352  irredrmul  20396  drngnidl  21216  znunit  21537  tgcl  22924  neiint  23059  restopnb  23130  ordtrest2lem  23158  pnfnei  23175  mnfnei  23176  iscnp4  23218  haust1  23307  ordthauslem  23338  tgcmp  23356  t1connperf  23391  2ndc1stc  23406  2ndcdisj  23411  islly2  23439  nllyrest  23441  reftr  23469  comppfsc  23487  ptbasfi  23536  ptcnp  23577  xkococnlem  23614  tgqtop  23667  fbssfi  23792  fgabs  23834  neifil  23835  trfil2  23842  elfm2  23903  elfm3  23905  rnelfmlem  23907  fmfnfmlem4  23912  flffbas  23950  fclsfnflim  23982  ptcmplem4  24010  tsmsxp  24110  blssexps  24382  blssex  24383  icccmplem3  24783  cnheibor  24924  pi1blem  25009  iscfil3  25244  iscmet3lem2  25263  metsscmetcld  25286  ovolicc2  25494  nulmbl2  25508  volsup  25528  dyadmbllem  25571  itg2const2  25713  bddmulibl  25811  bddiblnc  25814  limcflf  25853  itgsubst  26027  ulmdvlem3  26382  xrlimcnp  26948  amgm  26971  dchrptlem2  27246  lgsne0  27316  lgsqr  27332  lgsquadlem1  27361  dchrvmasumif  27484  rpvmasum2  27493  dchrisum0re  27494  dchrisum0lem3  27500  dchrisum0  27501  dchrmusum  27505  dchrvmasum  27506  chpdifbnd  27536  pntrlog2bnd  27565  pntibndlem3  27573  pntibnd  27574  pntleml  27592  ostth  27620  nosupno  27685  nosupbnd1lem1  27690  nosupbnd2  27698  noinfno  27700  noinfbnd1lem1  27705  noinfbnd2  27713  scutbdaybnd2  27798  oldlim  27862  oldbdayim  27864  sleadd1  27959  norecdiv  28153  precsexlem11  28178  noseqrdgfn  28249  brbtwn2  28851  colinearalg  28856  nbumgrvtx  29292  cusgrfilem1  29402  nmobndi  30723  spansneleq  31518  ofrn2  32586  xreceu  32849  ordtrest2NEWlem  33896  dya2iocnei  34259  connpconn  35215  cvmsss2  35254  cvmlift2lem10  35292  cvmlift3lem2  35300  outsidele  36108  neibastop1  36335  neibastop2lem  36336  matunitlindflem1  37598  mblfinlem1  37639  mblfinlem3  37641  mblfinlem4  37642  ismblfin  37643  cnambfre  37650  itg2addnclem  37653  itg2addnclem3  37655  ftc1anclem7  37681  ftc1anc  37683  fdc  37727  sstotbnd2  37756  sstotbnd  37757  isbndx  37764  ssbnd  37770  totbndbnd  37771  heibor  37803  unichnidl  38013  pexmidlem8N  39954  sn-0tie0  42448  nna4b4nsq  42649  elrfi  42683  fnwe2lem2  43041  hbtlem5  43118  rexlimdvaacbv  44195  rexlimddvcbvw  44196  relpfrlem  44946  liminfval2  45755  2zrngamgm  48134