Theorem rexlimdvaa 3134

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  ∃wrex 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3057

This theorem is referenced by:  rexlimddv  3139  tz7.7  6332  isofrlem  7274  nnawordex  8552  nnaordex2  8554  oaabs2  8564  fiin  9306  marypha1lem  9317  wemaplem3  9434  cantnflt  9562  fseqenlem2  9916  cardaleph  9980  coftr  10164  fin23lem26  10216  fin1a2lem13  10303  fpwwe2  10534  r1wunlim  10628  wunex2  10629  inttsk  10665  grur1  10711  inaprc  10727  receu  11762  zsupss  12835  xralrple  13104  rexanuz  15253  limsupval2  15387  caucvgb  15587  fsumiun  15728  rpnnen2lem12  16134  dvdsval2  16166  prmind2  16596  prmdvdsncoprmbd  16638  pcprmpw2  16794  pockthg  16818  prmreclem5  16832  vdwlem6  16898  vdwlem10  16902  sscpwex  17722  drsdirfi  18211  psgnunilem3  19409  sylow3lem2  19541  efgsfo  19652  lt6abl  19808  ghmcyg  19809  ablsimpgfind  20025  unitgrp  20302  irredrmul  20346  drngnidl  21181  znunit  21501  tgcl  22885  neiint  23020  restopnb  23091  ordtrest2lem  23119  pnfnei  23136  mnfnei  23137  iscnp4  23179  haust1  23268  ordthauslem  23299  tgcmp  23317  t1connperf  23352  2ndc1stc  23367  2ndcdisj  23372  islly2  23400  nllyrest  23402  reftr  23430  comppfsc  23448  ptbasfi  23497  ptcnp  23538  xkococnlem  23575  tgqtop  23628  fbssfi  23753  fgabs  23795  neifil  23796  trfil2  23803  elfm2  23864  elfm3  23866  rnelfmlem  23868  fmfnfmlem4  23873  flffbas  23911  fclsfnflim  23943  ptcmplem4  23971  tsmsxp  24071  blssexps  24342  blssex  24343  icccmplem3  24741  cnheibor  24882  pi1blem  24967  iscfil3  25201  iscmet3lem2  25220  metsscmetcld  25243  ovolicc2  25451  nulmbl2  25465  volsup  25485  dyadmbllem  25528  itg2const2  25670  bddmulibl  25768  bddiblnc  25771  limcflf  25810  itgsubst  25984  ulmdvlem3  26339  xrlimcnp  26906  amgm  26929  dchrptlem2  27204  lgsne0  27274  lgsqr  27290  lgsquadlem1  27319  dchrvmasumif  27442  rpvmasum2  27451  dchrisum0re  27452  dchrisum0lem3  27458  dchrisum0  27459  dchrmusum  27463  dchrvmasum  27464  chpdifbnd  27494  pntrlog2bnd  27523  pntibndlem3  27531  pntibnd  27532  pntleml  27550  ostth  27578  nosupno  27643  nosupbnd1lem1  27648  nosupbnd2  27656  noinfno  27658  noinfbnd1lem1  27663  noinfbnd2  27671  scutbdaybnd2  27758  oldlim  27833  oldbdayim  27835  sleadd1  27933  norecdiv  28130  precsexlem11  28156  noseqrdgfn  28237  pw2recs  28362  zs12ge0  28394  brbtwn2  28884  colinearalg  28889  nbumgrvtx  29325  cusgrfilem1  29435  nmobndi  30753  spansneleq  31548  ofrn2  32620  xreceu  32900  ordtrest2NEWlem  33933  dya2iocnei  34293  connpconn  35277  cvmsss2  35316  cvmlift2lem10  35354  cvmlift3lem2  35362  outsidele  36172  neibastop1  36399  neibastop2lem  36400  matunitlindflem1  37662  mblfinlem1  37703  mblfinlem3  37705  mblfinlem4  37706  ismblfin  37707  cnambfre  37714  itg2addnclem  37717  itg2addnclem3  37719  ftc1anclem7  37745  ftc1anc  37747  fdc  37791  sstotbnd2  37820  sstotbnd  37821  isbndx  37828  ssbnd  37834  totbndbnd  37835  heibor  37867  unichnidl  38077  pexmidlem8N  40022  sn-0tie0  42490  nna4b4nsq  42699  elrfi  42733  fnwe2lem2  43090  hbtlem5  43167  rexlimdvaacbv  44244  rexlimddvcbvw  44245  relpfrlem  44992  liminfval2  45812  2zrngamgm  48282