Theorem rexlimdvaa 3138

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  rexlimddv  3143  tz7.7  6343  isofrlem  7286  nnawordex  8565  nnaordex2  8567  oaabs2  8577  fiin  9325  marypha1lem  9336  wemaplem3  9453  cantnflt  9581  fseqenlem2  9935  cardaleph  9999  coftr  10183  fin23lem26  10235  fin1a2lem13  10322  fpwwe2  10554  r1wunlim  10648  wunex2  10649  inttsk  10685  grur1  10731  inaprc  10747  receu  11782  zsupss  12850  xralrple  13120  rexanuz  15269  limsupval2  15403  caucvgb  15603  fsumiun  15744  rpnnen2lem12  16150  dvdsval2  16182  prmind2  16612  prmdvdsncoprmbd  16654  pcprmpw2  16810  pockthg  16834  prmreclem5  16848  vdwlem6  16914  vdwlem10  16918  sscpwex  17739  drsdirfi  18228  psgnunilem3  19425  sylow3lem2  19557  efgsfo  19668  lt6abl  19824  ghmcyg  19825  ablsimpgfind  20041  unitgrp  20319  irredrmul  20363  drngnidl  21198  znunit  21518  tgcl  22913  neiint  23048  restopnb  23119  ordtrest2lem  23147  pnfnei  23164  mnfnei  23165  iscnp4  23207  haust1  23296  ordthauslem  23327  tgcmp  23345  t1connperf  23380  2ndc1stc  23395  2ndcdisj  23400  islly2  23428  nllyrest  23430  reftr  23458  comppfsc  23476  ptbasfi  23525  ptcnp  23566  xkococnlem  23603  tgqtop  23656  fbssfi  23781  fgabs  23823  neifil  23824  trfil2  23831  elfm2  23892  elfm3  23894  rnelfmlem  23896  fmfnfmlem4  23901  flffbas  23939  fclsfnflim  23971  ptcmplem4  23999  tsmsxp  24099  blssexps  24370  blssex  24371  icccmplem3  24769  cnheibor  24910  pi1blem  24995  iscfil3  25229  iscmet3lem2  25248  metsscmetcld  25271  ovolicc2  25479  nulmbl2  25493  volsup  25513  dyadmbllem  25556  itg2const2  25698  bddmulibl  25796  bddiblnc  25799  limcflf  25838  itgsubst  26012  ulmdvlem3  26367  xrlimcnp  26934  amgm  26957  dchrptlem2  27232  lgsne0  27302  lgsqr  27318  lgsquadlem1  27347  dchrvmasumif  27470  rpvmasum2  27479  dchrisum0re  27480  dchrisum0lem3  27486  dchrisum0  27487  dchrmusum  27491  dchrvmasum  27492  chpdifbnd  27522  pntrlog2bnd  27551  pntibndlem3  27559  pntibnd  27560  pntleml  27578  ostth  27606  nosupno  27671  nosupbnd1lem1  27676  nosupbnd2  27684  noinfno  27686  noinfbnd1lem1  27691  noinfbnd2  27699  cutbdaybnd2  27792  oldlim  27883  oldbdayim  27885  leadds1  27985  norecdiv  28186  precsexlem11  28213  noseqrdgfn  28302  pw2recs  28434  z12sge0  28479  brbtwn2  28978  colinearalg  28983  nbumgrvtx  29419  cusgrfilem1  29529  nmobndi  30850  spansneleq  31645  ofrn2  32718  xreceu  33003  ordtrest2NEWlem  34079  dya2iocnei  34439  connpconn  35429  cvmsss2  35468  cvmlift2lem10  35506  cvmlift3lem2  35514  outsidele  36326  neibastop1  36553  neibastop2lem  36554  matunitlindflem1  37817  mblfinlem1  37858  mblfinlem3  37860  mblfinlem4  37861  ismblfin  37862  cnambfre  37869  itg2addnclem  37872  itg2addnclem3  37874  ftc1anclem7  37900  ftc1anc  37902  fdc  37946  sstotbnd2  37975  sstotbnd  37976  isbndx  37983  ssbnd  37989  totbndbnd  37990  heibor  38022  unichnidl  38232  pexmidlem8N  40237  sn-0tie0  42706  nna4b4nsq  42903  elrfi  42936  fnwe2lem2  43293  hbtlem5  43370  rexlimdvaacbv  44446  rexlimddvcbvw  44447  relpfrlem  45194  liminfval2  46012  2zrngamgm  48491