Theorem rexlimdvaa 3156

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-rex 3071

This theorem is referenced by:  rexlimddv  3161  tz7.7  6390  isofrlem  7339  nnawordex  8639  oaabs2  8650  fiin  9419  marypha1lem  9430  wemaplem3  9545  cantnflt  9669  fseqenlem2  10022  cardaleph  10086  coftr  10270  fin23lem26  10322  fin1a2lem13  10409  fpwwe2  10640  r1wunlim  10734  wunex2  10735  inttsk  10771  grur1  10817  inaprc  10833  receu  11861  zsupss  12923  xralrple  13186  rexanuz  15294  limsupval2  15426  caucvgb  15628  fsumiun  15769  rpnnen2lem12  16170  dvdsval2  16202  prmind2  16624  prmdvdsncoprmbd  16665  pcprmpw2  16817  pockthg  16841  prmreclem5  16855  vdwlem6  16921  vdwlem10  16925  sscpwex  17764  drsdirfi  18260  psgnunilem3  19366  sylow3lem2  19498  efgsfo  19609  lt6abl  19765  ghmcyg  19766  ablsimpgfind  19982  unitgrp  20201  irredrmul  20245  drngnidl  20860  znunit  21125  tgcl  22479  neiint  22615  restopnb  22686  ordtrest2lem  22714  pnfnei  22731  mnfnei  22732  iscnp4  22774  haust1  22863  ordthauslem  22894  tgcmp  22912  t1connperf  22947  2ndc1stc  22962  2ndcdisj  22967  islly2  22995  nllyrest  22997  reftr  23025  comppfsc  23043  ptbasfi  23092  ptcnp  23133  xkococnlem  23170  tgqtop  23223  fbssfi  23348  fgabs  23390  neifil  23391  trfil2  23398  elfm2  23459  elfm3  23461  rnelfmlem  23463  fmfnfmlem4  23468  flffbas  23506  fclsfnflim  23538  ptcmplem4  23566  tsmsxp  23666  blssexps  23939  blssex  23940  icccmplem3  24347  cnheibor  24478  pi1blem  24562  iscfil3  24797  iscmet3lem2  24816  metsscmetcld  24839  ovolicc2  25046  nulmbl2  25060  volsup  25080  dyadmbllem  25123  itg2const2  25266  bddmulibl  25363  bddiblnc  25366  limcflf  25405  itgsubst  25573  ulmdvlem3  25921  xrlimcnp  26480  amgm  26502  dchrptlem2  26775  lgsne0  26845  lgsqr  26861  lgsquadlem1  26890  dchrvmasumif  27013  rpvmasum2  27022  dchrisum0re  27023  dchrisum0lem3  27029  dchrisum0  27030  dchrmusum  27034  dchrvmasum  27035  chpdifbnd  27065  pntrlog2bnd  27094  pntibndlem3  27102  pntibnd  27103  pntleml  27121  ostth  27149  nosupno  27213  nosupbnd1lem1  27218  nosupbnd2  27226  noinfno  27228  noinfbnd1lem1  27233  noinfbnd2  27241  scutbdaybnd2  27325  oldlim  27389  oldbdayim  27391  sleadd1  27482  norecdiv  27648  precsexlem11  27673  brbtwn2  28201  colinearalg  28206  nbumgrvtx  28641  cusgrfilem1  28750  nmobndi  30066  spansneleq  30861  ofrn2  31903  xreceu  32126  ordtrest2NEWlem  32971  dya2iocnei  33350  connpconn  34295  cvmsss2  34334  cvmlift2lem10  34372  cvmlift3lem2  34380  outsidele  35173  neibastop1  35330  neibastop2lem  35331  matunitlindflem1  36570  mblfinlem1  36611  mblfinlem3  36613  mblfinlem4  36614  ismblfin  36615  cnambfre  36622  itg2addnclem  36625  itg2addnclem3  36627  ftc1anclem7  36653  ftc1anc  36655  fdc  36699  sstotbnd2  36728  sstotbnd  36729  isbndx  36736  ssbnd  36742  totbndbnd  36743  heibor  36775  unichnidl  36985  pexmidlem8N  38934  sn-0tie0  41394  nna4b4nsq  41484  elrfi  41514  fnwe2lem2  41875  hbtlem5  41952  rexlimdvaacbv  43039  rexlimddvcbvw  43040  liminfval2  44563  2zrngamgm  46916