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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3061

This theorem is referenced by:  rexlimddv  3147  tz7.7  6378  isofrlem  7332  nnawordex  8647  nnaordex2  8649  oaabs2  8659  fiin  9432  marypha1lem  9443  wemaplem3  9560  cantnflt  9684  fseqenlem2  10037  cardaleph  10101  coftr  10285  fin23lem26  10337  fin1a2lem13  10424  fpwwe2  10655  r1wunlim  10749  wunex2  10750  inttsk  10786  grur1  10832  inaprc  10848  receu  11880  zsupss  12951  xralrple  13219  rexanuz  15362  limsupval2  15494  caucvgb  15694  fsumiun  15835  rpnnen2lem12  16241  dvdsval2  16273  prmind2  16702  prmdvdsncoprmbd  16744  pcprmpw2  16900  pockthg  16924  prmreclem5  16938  vdwlem6  17004  vdwlem10  17008  sscpwex  17826  drsdirfi  18315  psgnunilem3  19475  sylow3lem2  19607  efgsfo  19718  lt6abl  19874  ghmcyg  19875  ablsimpgfind  20091  unitgrp  20341  irredrmul  20385  drngnidl  21202  znunit  21522  tgcl  22905  neiint  23040  restopnb  23111  ordtrest2lem  23139  pnfnei  23156  mnfnei  23157  iscnp4  23199  haust1  23288  ordthauslem  23319  tgcmp  23337  t1connperf  23372  2ndc1stc  23387  2ndcdisj  23392  islly2  23420  nllyrest  23422  reftr  23450  comppfsc  23468  ptbasfi  23517  ptcnp  23558  xkococnlem  23595  tgqtop  23648  fbssfi  23773  fgabs  23815  neifil  23816  trfil2  23823  elfm2  23884  elfm3  23886  rnelfmlem  23888  fmfnfmlem4  23893  flffbas  23931  fclsfnflim  23963  ptcmplem4  23991  tsmsxp  24091  blssexps  24363  blssex  24364  icccmplem3  24762  cnheibor  24903  pi1blem  24988  iscfil3  25223  iscmet3lem2  25242  metsscmetcld  25265  ovolicc2  25473  nulmbl2  25487  volsup  25507  dyadmbllem  25550  itg2const2  25692  bddmulibl  25790  bddiblnc  25793  limcflf  25832  itgsubst  26006  ulmdvlem3  26361  xrlimcnp  26928  amgm  26951  dchrptlem2  27226  lgsne0  27296  lgsqr  27312  lgsquadlem1  27341  dchrvmasumif  27464  rpvmasum2  27473  dchrisum0re  27474  dchrisum0lem3  27480  dchrisum0  27481  dchrmusum  27485  dchrvmasum  27486  chpdifbnd  27516  pntrlog2bnd  27545  pntibndlem3  27553  pntibnd  27554  pntleml  27572  ostth  27600  nosupno  27665  nosupbnd1lem1  27670  nosupbnd2  27678  noinfno  27680  noinfbnd1lem1  27685  noinfbnd2  27693  scutbdaybnd2  27778  oldlim  27842  oldbdayim  27844  sleadd1  27939  norecdiv  28133  precsexlem11  28158  noseqrdgfn  28229  brbtwn2  28830  colinearalg  28835  nbumgrvtx  29271  cusgrfilem1  29381  nmobndi  30702  spansneleq  31497  ofrn2  32564  xreceu  32842  ordtrest2NEWlem  33899  dya2iocnei  34260  connpconn  35203  cvmsss2  35242  cvmlift2lem10  35280  cvmlift3lem2  35288  outsidele  36096  neibastop1  36323  neibastop2lem  36324  matunitlindflem1  37586  mblfinlem1  37627  mblfinlem3  37629  mblfinlem4  37630  ismblfin  37631  cnambfre  37638  itg2addnclem  37641  itg2addnclem3  37643  ftc1anclem7  37669  ftc1anc  37671  fdc  37715  sstotbnd2  37744  sstotbnd  37745  isbndx  37752  ssbnd  37758  totbndbnd  37759  heibor  37791  unichnidl  38001  pexmidlem8N  39942  sn-0tie0  42429  nna4b4nsq  42630  elrfi  42664  fnwe2lem2  43022  hbtlem5  43099  rexlimdvaacbv  44176  rexlimddvcbvw  44177  relpfrlem  44926  liminfval2  45745  2zrngamgm  48168