Theorem rexlimdvaa 3169

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

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

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 3092

This theorem is used by:  rexlimddv  3174  tz7.7  6390  isofrlem  7344  nnawordex  8625  nnaordex2  8627  oaabs2  8637  fiin  9385  marypha1lem  9396  wemaplem3  9513  cantnflt  9644  fseqenlem2  10021  cardaleph  10085  coftr  10268  fin23lem26  10320  fin1a2lem13  10407  fpwwe2  10639  r1wunlim  10733  wunex2  10734  inttsk  10770  grur1  10816  inaprc  10832  receu  11870  zsupss  12972  xralrple  13242  rexanuz  15416  limsupval2  15550  caucvgb  15750  fsumiun  15891  rpnnen2lem12  16298  dvdsval2  16330  prmind2  16760  prmdvdsncoprmbd  16803  pcprmpw2  16959  pockthg  16983  prmreclem5  16997  vdwlem6  17063  vdwlem10  17067  sscpwex  17889  drsdirfi  18378  0gisid  18743  psgnunilem3  19589  sylow3lem2  19721  efgsfo  19832  lt6abl  19988  ghmcyg  19989  ablsimpgfind  20205  unitgrp  20490  irredrmul  20534  unichnlidl  21391  drngnidl  21406  znunit  21742  tgcl  23155  neiint  23290  restopnb  23361  ordtrest2lem  23389  pnfnei  23406  mnfnei  23407  iscnp4  23449  haust1  23538  ordthauslem  23569  tgcmp  23587  t1connperf  23622  2ndc1stc  23637  2ndcdisj  23642  islly2  23670  nllyrest  23672  reftr  23700  comppfsc  23718  ptbasfi  23767  ptcnp  23808  xkococnlem  23845  tgqtop  23898  fbssfi  24023  fgabs  24065  neifil  24066  trfil2  24073  elfm2  24134  elfm3  24136  rnelfmlem  24138  fmfnfmlem4  24143  flffbas  24181  fclsfnflim  24213  ptcmplem4  24241  tsmsxp  24341  blssexps  24612  blssex  24613  icccmplem3  25011  cnheibor  25143  pi1blem  25227  iscfil3  25461  iscmet3lem2  25480  metsscmetcld  25503  ovolicc2  25710  nulmbl2  25724  volsup  25744  dyadmbllem  25787  itg2const2  25929  bddmulibl  26027  bddiblnc  26030  limcflf  26069  itgsubst  26237  ulmdvlem3  26594  xrlimcnp  27162  amgm  27184  dchrptlem2  27458  lgsne0  27528  lgsqr  27544  lgsquadlem1  27573  dchrvmasumif  27696  rpvmasum2  27705  dchrisum0re  27706  dchrisum0lem3  27712  dchrisum0  27713  dchrmusum  27717  dchrvmasum  27718  chpdifbnd  27748  pntrlog2bnd  27777  pntibndlem3  27785  pntibnd  27786  pntleml  27804  ostth  27832  nosupno  27896  nosupbnd1lem1  27901  nosupbnd2  27909  noinfno  27911  noinfbnd1lem1  27916  noinfbnd2  27924  cutbdaybnd2  28018  oldlim  28109  oldbdayim  28111  leadds1  28211  norecdiv  28412  precsexlem11  28439  noseqrdgfn  28528  pw2recs  28660  z12sge0  28705  brbtwn2  29284  colinearalg  29289  nbumgrvtx  29725  cusgrfilem1  29834  nmobndi  31156  spansneleq  31951  ofrn2  33014  xreceu  33270  ordtrest2NEWlem  34335  dya2iocnei  34696  connpconn  35740  cvmsss2  35779  cvmlift2lem10  35817  cvmlift3lem2  35825  outsidele  36637  ltnadd  36723  nadddilem4  36728  neibastop1  36903  neibastop2lem  36904  ttctr  37037  dfttc2g  37050  dfttc4  37074  mh-inf3f1  37085  matunitlindflem1  38300  mblfinlem1  38341  mblfinlem3  38343  mblfinlem4  38344  ismblfin  38345  cnambfre  38352  itg2addnclem  38355  itg2addnclem3  38357  ftc1anclem7  38383  ftc1anc  38385  fdc  38429  sstotbnd2  38458  sstotbnd  38459  isbndx  38466  ssbnd  38472  totbndbnd  38473  heibor  38505  unichnidl  38715  pexmidlem8N  40784  sn-0tie0  43258  nna4b4nsq  43425  elrfi  43458  fnwe2lem2  43811  hbtlem5  43888  rexlimdvaacbv  44962  rexlimddvcbvw  44963  relpfrlem  45695  liminfval2  46515  2zrngamgm  49043