Theorem rexlimdvaa 3164

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3087

This theorem is used by:  rexlimddv  3169  tz7.7  6383  isofrlem  7341  nnawordex  8625  nnaordex2  8627  oaabs2  8637  fiin  9392  marypha1lem  9403  wemaplem3  9520  cantnflt  9651  fseqenlem2  10028  cardaleph  10092  coftr  10275  fin23lem26  10327  fin1a2lem13  10414  fpwwe2  10652  r1wunlim  10746  wunex2  10747  inttsk  10783  grur1  10829  inaprc  10845  receu  11883  zsupss  12986  xralrple  13257  rexanuz  15433  limsupval2  15567  caucvgb  15767  fsumiun  15908  rpnnen2lem12  16313  dvdsval2  16345  prmind2  16775  prmdvdsncoprmbd  16818  pcprmpw2  16974  pockthg  16998  prmreclem5  17012  vdwlem6  17078  vdwlem10  17082  sscpwex  17904  drsdirfi  18393  0gisid  18761  psgnunilem3  19623  sylow3lem2  19755  efgsfo  19866  lt6abl  20022  ghmcyg  20023  ablsimpgfind  20239  unitgrp  20524  irredrmul  20568  unichnlidl  21425  drngnidl  21440  znunit  21776  matunitlindflem1  22901  tgcl  23194  neiint  23329  restopnb  23400  ordtrest2lem  23428  pnfnei  23445  mnfnei  23446  iscnp4  23488  haust1  23577  ordthauslem  23608  tgcmp  23626  t1connperf  23661  2ndc1stc  23676  2ndcdisj  23682  islly2  23710  nllyrest  23712  reftr  23740  comppfsc  23758  ptbasfi  23807  ptcnp  23848  xkococnlem  23885  tgqtop  23938  fbssfi  24063  fgabs  24105  neifil  24106  trfil2  24113  elfm2  24174  elfm3  24176  rnelfmlem  24178  fmfnfmlem4  24183  flffbas  24221  fclsfnflim  24253  ptcmplem4  24281  tsmsxp  24381  blssexps  24652  blssex  24653  icccmplem3  25051  cnheibor  25183  pi1blem  25267  iscfil3  25501  iscmet3lem2  25520  metsscmetcld  25543  ovolicc2  25750  nulmbl2  25764  volsup  25784  dyadmbllem  25827  itg2const2  25969  bddmulibl  26066  bddiblnc  26069  limcflf  26108  itgsubst  26276  ulmdvlem3  26638  xrlimcnp  27205  amgm  27227  dchrptlem2  27501  lgsne0  27571  lgsqr  27587  lgsquadlem1  27616  dchrvmasumif  27739  rpvmasum2  27748  dchrisum0re  27749  dchrisum0lem3  27755  dchrisum0  27756  dchrmusum  27760  dchrvmasum  27761  chpdifbnd  27791  pntrlog2bnd  27820  pntibndlem3  27828  pntibnd  27829  pntleml  27847  ostth  27875  nosupno  27939  nosupbnd1lem1  27944  nosupbnd2  27952  noinfno  27954  noinfbnd1lem1  27959  noinfbnd2  27967  cutbdaybnd2  28061  oldlim  28152  oldbdayim  28154  leadds1  28254  norecdiv  28455  precsexlem11  28482  noseqrdgfn  28571  pw2recs  28703  z12sge0  28748  brbtwn2  29362  colinearalg  29367  nbumgrvtx  29806  cusgrfilem1  29915  nmobndi  31256  spansneleq  32051  ofrn2  33113  xreceu  33367  ordtrest2NEWlem  34432  dya2iocnei  34793  connpconn  35814  cvmsss2  35853  cvmlift2lem10  35891  cvmlift3lem2  35899  outsidele  36712  ltnadd  36798  nadddilem4  36803  neibastop1  36978  neibastop2lem  36979  ttctr  37112  dfttc2g  37125  dfttc4  37149  mh-inf3f1  37160  mblfinlem1  38406  mblfinlem3  38408  mblfinlem4  38409  ismblfin  38410  cnambfre  38417  itg2addnclem  38420  itg2addnclem3  38422  ftc1anclem7  38448  ftc1anc  38450  fdc  38495  sstotbnd2  38524  sstotbnd  38525  isbndx  38532  ssbnd  38538  totbndbnd  38539  heibor  38571  unichnidl  38781  pexmidlem8N  40850  sn-0tie0  43339  nna4b4nsq  43506  elrfi  43539  fnwe2lem2  43892  hbtlem5  43969  rexlimdvaacbv  45043  rexlimddvcbvw  45044  relpfrlem  45776  liminfval2  46596  2zrngamgm  49160