Theorem rexlimdvaa 3142

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-rex 3065

This theorem is referenced by:  rexlimddv  3147  tz7.7  6343  isofrlem  7291  nnawordex  8570  nnaordex2  8572  oaabs2  8582  fiin  9332  marypha1lem  9343  wemaplem3  9460  cantnflt  9591  fseqenlem2  9945  cardaleph  10009  coftr  10193  fin23lem26  10245  fin1a2lem13  10332  fpwwe2  10564  r1wunlim  10658  wunex2  10659  inttsk  10695  grur1  10741  inaprc  10757  receu  11793  zsupss  12885  xralrple  13155  rexanuz  15306  limsupval2  15440  caucvgb  15640  fsumiun  15782  rpnnen2lem12  16190  dvdsval2  16222  prmind2  16652  prmdvdsncoprmbd  16695  pcprmpw2  16851  pockthg  16875  prmreclem5  16889  vdwlem6  16955  vdwlem10  16959  sscpwex  17780  drsdirfi  18269  psgnunilem3  19469  sylow3lem2  19601  efgsfo  19712  lt6abl  19868  ghmcyg  19869  ablsimpgfind  20085  unitgrp  20361  irredrmul  20405  drngnidl  21243  znunit  21545  tgcl  22959  neiint  23094  restopnb  23165  ordtrest2lem  23193  pnfnei  23210  mnfnei  23211  iscnp4  23253  haust1  23342  ordthauslem  23373  tgcmp  23391  t1connperf  23426  2ndc1stc  23441  2ndcdisj  23446  islly2  23474  nllyrest  23476  reftr  23504  comppfsc  23522  ptbasfi  23571  ptcnp  23612  xkococnlem  23649  tgqtop  23702  fbssfi  23827  fgabs  23869  neifil  23870  trfil2  23877  elfm2  23938  elfm3  23940  rnelfmlem  23942  fmfnfmlem4  23947  flffbas  23985  fclsfnflim  24017  ptcmplem4  24045  tsmsxp  24145  blssexps  24416  blssex  24417  icccmplem3  24815  cnheibor  24947  pi1blem  25031  iscfil3  25265  iscmet3lem2  25284  metsscmetcld  25307  ovolicc2  25514  nulmbl2  25528  volsup  25548  dyadmbllem  25591  itg2const2  25733  bddmulibl  25831  bddiblnc  25834  limcflf  25873  itgsubst  26041  ulmdvlem3  26392  xrlimcnp  26957  amgm  26979  dchrptlem2  27253  lgsne0  27323  lgsqr  27339  lgsquadlem1  27368  dchrvmasumif  27491  rpvmasum2  27500  dchrisum0re  27501  dchrisum0lem3  27507  dchrisum0  27508  dchrmusum  27512  dchrvmasum  27513  chpdifbnd  27543  pntrlog2bnd  27572  pntibndlem3  27580  pntibnd  27581  pntleml  27599  ostth  27627  nosupno  27692  nosupbnd1lem1  27697  nosupbnd2  27705  noinfno  27707  noinfbnd1lem1  27712  noinfbnd2  27720  cutbdaybnd2  27813  oldlim  27904  oldbdayim  27906  leadds1  28006  norecdiv  28207  precsexlem11  28234  noseqrdgfn  28323  pw2recs  28455  z12sge0  28500  brbtwn2  28999  colinearalg  29004  nbumgrvtx  29440  cusgrfilem1  29549  nmobndi  30871  spansneleq  31666  ofrn2  32739  xreceu  33007  ordtrest2NEWlem  34113  dya2iocnei  34473  connpconn  35470  cvmsss2  35509  cvmlift2lem10  35547  cvmlift3lem2  35555  outsidele  36367  neibastop1  36594  neibastop2lem  36595  ttctr  36728  dfttc2g  36741  dfttc4  36765  mh-inf3f1  36776  matunitlindflem1  37990  mblfinlem1  38031  mblfinlem3  38033  mblfinlem4  38034  ismblfin  38035  cnambfre  38042  itg2addnclem  38045  itg2addnclem3  38047  ftc1anclem7  38073  ftc1anc  38075  fdc  38119  sstotbnd2  38148  sstotbnd  38149  isbndx  38156  ssbnd  38162  totbndbnd  38163  heibor  38195  unichnidl  38405  pexmidlem8N  40476  sn-0tie0  42948  nna4b4nsq  43117  elrfi  43150  fnwe2lem2  43503  hbtlem5  43580  rexlimdvaacbv  44656  rexlimddvcbvw  44657  relpfrlem  45404  liminfval2  46218  2zrngamgm  48743