Theorem rexlimdvaa 3131

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

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

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 3054

This theorem is referenced by:  rexlimddv  3136  tz7.7  6337  isofrlem  7281  nnawordex  8562  nnaordex2  8564  oaabs2  8574  fiin  9331  marypha1lem  9342  wemaplem3  9459  cantnflt  9587  fseqenlem2  9938  cardaleph  10002  coftr  10186  fin23lem26  10238  fin1a2lem13  10325  fpwwe2  10556  r1wunlim  10650  wunex2  10651  inttsk  10687  grur1  10733  inaprc  10749  receu  11783  zsupss  12856  xralrple  13125  rexanuz  15271  limsupval2  15405  caucvgb  15605  fsumiun  15746  rpnnen2lem12  16152  dvdsval2  16184  prmind2  16614  prmdvdsncoprmbd  16656  pcprmpw2  16812  pockthg  16836  prmreclem5  16850  vdwlem6  16916  vdwlem10  16920  sscpwex  17740  drsdirfi  18229  psgnunilem3  19393  sylow3lem2  19525  efgsfo  19636  lt6abl  19792  ghmcyg  19793  ablsimpgfind  20009  unitgrp  20286  irredrmul  20330  drngnidl  21168  znunit  21488  tgcl  22872  neiint  23007  restopnb  23078  ordtrest2lem  23106  pnfnei  23123  mnfnei  23124  iscnp4  23166  haust1  23255  ordthauslem  23286  tgcmp  23304  t1connperf  23339  2ndc1stc  23354  2ndcdisj  23359  islly2  23387  nllyrest  23389  reftr  23417  comppfsc  23435  ptbasfi  23484  ptcnp  23525  xkococnlem  23562  tgqtop  23615  fbssfi  23740  fgabs  23782  neifil  23783  trfil2  23790  elfm2  23851  elfm3  23853  rnelfmlem  23855  fmfnfmlem4  23860  flffbas  23898  fclsfnflim  23930  ptcmplem4  23958  tsmsxp  24058  blssexps  24330  blssex  24331  icccmplem3  24729  cnheibor  24870  pi1blem  24955  iscfil3  25189  iscmet3lem2  25208  metsscmetcld  25231  ovolicc2  25439  nulmbl2  25453  volsup  25473  dyadmbllem  25516  itg2const2  25658  bddmulibl  25756  bddiblnc  25759  limcflf  25798  itgsubst  25972  ulmdvlem3  26327  xrlimcnp  26894  amgm  26917  dchrptlem2  27192  lgsne0  27262  lgsqr  27278  lgsquadlem1  27307  dchrvmasumif  27430  rpvmasum2  27439  dchrisum0re  27440  dchrisum0lem3  27446  dchrisum0  27447  dchrmusum  27451  dchrvmasum  27452  chpdifbnd  27482  pntrlog2bnd  27511  pntibndlem3  27519  pntibnd  27520  pntleml  27538  ostth  27566  nosupno  27631  nosupbnd1lem1  27636  nosupbnd2  27644  noinfno  27646  noinfbnd1lem1  27651  noinfbnd2  27659  scutbdaybnd2  27745  oldlim  27819  oldbdayim  27821  sleadd1  27919  norecdiv  28116  precsexlem11  28142  noseqrdgfn  28223  pw2recs  28348  zs12ge0  28378  brbtwn2  28868  colinearalg  28873  nbumgrvtx  29309  cusgrfilem1  29419  nmobndi  30737  spansneleq  31532  ofrn2  32597  xreceu  32875  ordtrest2NEWlem  33891  dya2iocnei  34252  connpconn  35210  cvmsss2  35249  cvmlift2lem10  35287  cvmlift3lem2  35295  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  39959  sn-0tie0  42427  nna4b4nsq  42636  elrfi  42670  fnwe2lem2  43027  hbtlem5  43104  rexlimdvaacbv  44181  rexlimddvcbvw  44182  relpfrlem  44930  liminfval2  45753  2zrngamgm  48233