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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2121  ∃wrex 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-rex 3066

This theorem is referenced by:  rexlimddv  3148  tz7.7  6339  isofrlem  7287  nnawordex  8567  nnaordex2  8569  oaabs2  8579  fiin  9329  marypha1lem  9340  wemaplem3  9457  cantnflt  9588  fseqenlem2  9942  cardaleph  10006  coftr  10191  fin23lem26  10243  fin1a2lem13  10330  fpwwe2  10562  r1wunlim  10656  wunex2  10657  inttsk  10693  grur1  10739  inaprc  10755  receu  11791  zsupss  12882  xralrple  13152  rexanuz  15303  limsupval2  15437  caucvgb  15637  fsumiun  15779  rpnnen2lem12  16187  dvdsval2  16219  prmind2  16649  prmdvdsncoprmbd  16692  pcprmpw2  16848  pockthg  16872  prmreclem5  16886  vdwlem6  16952  vdwlem10  16956  sscpwex  17777  drsdirfi  18266  psgnunilem3  19465  sylow3lem2  19597  efgsfo  19708  lt6abl  19864  ghmcyg  19865  ablsimpgfind  20081  unitgrp  20357  irredrmul  20401  drngnidl  21239  znunit  21541  tgcl  22955  neiint  23090  restopnb  23161  ordtrest2lem  23189  pnfnei  23206  mnfnei  23207  iscnp4  23249  haust1  23338  ordthauslem  23369  tgcmp  23387  t1connperf  23422  2ndc1stc  23437  2ndcdisj  23442  islly2  23470  nllyrest  23472  reftr  23500  comppfsc  23518  ptbasfi  23567  ptcnp  23608  xkococnlem  23645  tgqtop  23698  fbssfi  23823  fgabs  23865  neifil  23866  trfil2  23873  elfm2  23934  elfm3  23936  rnelfmlem  23938  fmfnfmlem4  23943  flffbas  23981  fclsfnflim  24013  ptcmplem4  24041  tsmsxp  24141  blssexps  24412  blssex  24413  icccmplem3  24811  cnheibor  24943  pi1blem  25027  iscfil3  25261  iscmet3lem2  25280  metsscmetcld  25303  ovolicc2  25510  nulmbl2  25524  volsup  25544  dyadmbllem  25587  itg2const2  25729  bddmulibl  25827  bddiblnc  25830  limcflf  25869  itgsubst  26037  ulmdvlem3  26388  xrlimcnp  26953  amgm  26975  dchrptlem2  27249  lgsne0  27319  lgsqr  27335  lgsquadlem1  27364  dchrvmasumif  27487  rpvmasum2  27496  dchrisum0re  27497  dchrisum0lem3  27503  dchrisum0  27504  dchrmusum  27508  dchrvmasum  27509  chpdifbnd  27539  pntrlog2bnd  27568  pntibndlem3  27576  pntibnd  27577  pntleml  27595  ostth  27623  nosupno  27687  nosupbnd1lem1  27692  nosupbnd2  27700  noinfno  27702  noinfbnd1lem1  27707  noinfbnd2  27715  cutbdaybnd2  27808  oldlim  27899  oldbdayim  27901  leadds1  28001  norecdiv  28202  precsexlem11  28229  noseqrdgfn  28318  pw2recs  28450  z12sge0  28495  brbtwn2  28994  colinearalg  28999  nbumgrvtx  29435  cusgrfilem1  29544  nmobndi  30866  spansneleq  31661  ofrn2  32734  xreceu  33002  ordtrest2NEWlem  34116  dya2iocnei  34476  connpconn  35476  cvmsss2  35515  cvmlift2lem10  35553  cvmlift3lem2  35561  outsidele  36373  neibastop1  36600  neibastop2lem  36601  ttctr  36734  dfttc2g  36747  dfttc4  36771  mh-inf3f1  36782  matunitlindflem1  37996  mblfinlem1  38037  mblfinlem3  38039  mblfinlem4  38040  ismblfin  38041  cnambfre  38048  itg2addnclem  38051  itg2addnclem3  38053  ftc1anclem7  38079  ftc1anc  38081  fdc  38125  sstotbnd2  38154  sstotbnd  38155  isbndx  38162  ssbnd  38168  totbndbnd  38169  heibor  38201  unichnidl  38411  pexmidlem8N  40482  sn-0tie0  42954  nna4b4nsq  43123  elrfi  43156  fnwe2lem2  43509  hbtlem5  43586  rexlimdvaacbv  44662  rexlimddvcbvw  44663  relpfrlem  45410  liminfval2  46223  2zrngamgm  48748