Theorem rexlimdvaa 3135

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∃wrex 3053

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 3054

This theorem is referenced by:  rexlimddv  3140  tz7.7  6358  isofrlem  7315  nnawordex  8601  nnaordex2  8603  oaabs2  8613  fiin  9373  marypha1lem  9384  wemaplem3  9501  cantnflt  9625  fseqenlem2  9978  cardaleph  10042  coftr  10226  fin23lem26  10278  fin1a2lem13  10365  fpwwe2  10596  r1wunlim  10690  wunex2  10691  inttsk  10727  grur1  10773  inaprc  10789  receu  11823  zsupss  12896  xralrple  13165  rexanuz  15312  limsupval2  15446  caucvgb  15646  fsumiun  15787  rpnnen2lem12  16193  dvdsval2  16225  prmind2  16655  prmdvdsncoprmbd  16697  pcprmpw2  16853  pockthg  16877  prmreclem5  16891  vdwlem6  16957  vdwlem10  16961  sscpwex  17777  drsdirfi  18266  psgnunilem3  19426  sylow3lem2  19558  efgsfo  19669  lt6abl  19825  ghmcyg  19826  ablsimpgfind  20042  unitgrp  20292  irredrmul  20336  drngnidl  21153  znunit  21473  tgcl  22856  neiint  22991  restopnb  23062  ordtrest2lem  23090  pnfnei  23107  mnfnei  23108  iscnp4  23150  haust1  23239  ordthauslem  23270  tgcmp  23288  t1connperf  23323  2ndc1stc  23338  2ndcdisj  23343  islly2  23371  nllyrest  23373  reftr  23401  comppfsc  23419  ptbasfi  23468  ptcnp  23509  xkococnlem  23546  tgqtop  23599  fbssfi  23724  fgabs  23766  neifil  23767  trfil2  23774  elfm2  23835  elfm3  23837  rnelfmlem  23839  fmfnfmlem4  23844  flffbas  23882  fclsfnflim  23914  ptcmplem4  23942  tsmsxp  24042  blssexps  24314  blssex  24315  icccmplem3  24713  cnheibor  24854  pi1blem  24939  iscfil3  25173  iscmet3lem2  25192  metsscmetcld  25215  ovolicc2  25423  nulmbl2  25437  volsup  25457  dyadmbllem  25500  itg2const2  25642  bddmulibl  25740  bddiblnc  25743  limcflf  25782  itgsubst  25956  ulmdvlem3  26311  xrlimcnp  26878  amgm  26901  dchrptlem2  27176  lgsne0  27246  lgsqr  27262  lgsquadlem1  27291  dchrvmasumif  27414  rpvmasum2  27423  dchrisum0re  27424  dchrisum0lem3  27430  dchrisum0  27431  dchrmusum  27435  dchrvmasum  27436  chpdifbnd  27466  pntrlog2bnd  27495  pntibndlem3  27503  pntibnd  27504  pntleml  27522  ostth  27550  nosupno  27615  nosupbnd1lem1  27620  nosupbnd2  27628  noinfno  27630  noinfbnd1lem1  27635  noinfbnd2  27643  scutbdaybnd2  27728  oldlim  27798  oldbdayim  27800  sleadd1  27896  norecdiv  28093  precsexlem11  28119  noseqrdgfn  28200  pw2recs  28323  zs12ge0  28342  brbtwn2  28832  colinearalg  28837  nbumgrvtx  29273  cusgrfilem1  29383  nmobndi  30704  spansneleq  31499  ofrn2  32564  xreceu  32842  ordtrest2NEWlem  33912  dya2iocnei  34273  connpconn  35222  cvmsss2  35261  cvmlift2lem10  35299  cvmlift3lem2  35307  outsidele  36120  neibastop1  36347  neibastop2lem  36348  matunitlindflem1  37610  mblfinlem1  37651  mblfinlem3  37653  mblfinlem4  37654  ismblfin  37655  cnambfre  37662  itg2addnclem  37665  itg2addnclem3  37667  ftc1anclem7  37693  ftc1anc  37695  fdc  37739  sstotbnd2  37768  sstotbnd  37769  isbndx  37776  ssbnd  37782  totbndbnd  37783  heibor  37815  unichnidl  38025  pexmidlem8N  39971  sn-0tie0  42439  nna4b4nsq  42648  elrfi  42682  fnwe2lem2  43040  hbtlem5  43117  rexlimdvaacbv  44194  rexlimddvcbvw  44195  relpfrlem  44943  liminfval2  45766  2zrngamgm  48233