Theorem rexlimdvaa 3148

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2098  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-rex 3063

This theorem is referenced by:  rexlimddv  3153  tz7.7  6381  isofrlem  7330  nnawordex  8633  nnaordex2  8635  oaabs2  8645  fiin  9414  marypha1lem  9425  wemaplem3  9540  cantnflt  9664  fseqenlem2  10017  cardaleph  10081  coftr  10265  fin23lem26  10317  fin1a2lem13  10404  fpwwe2  10635  r1wunlim  10729  wunex2  10730  inttsk  10766  grur1  10812  inaprc  10828  receu  11857  zsupss  12919  xralrple  13182  rexanuz  15290  limsupval2  15422  caucvgb  15624  fsumiun  15765  rpnnen2lem12  16167  dvdsval2  16199  prmind2  16621  prmdvdsncoprmbd  16664  pcprmpw2  16816  pockthg  16840  prmreclem5  16854  vdwlem6  16920  vdwlem10  16924  sscpwex  17763  drsdirfi  18262  psgnunilem3  19408  sylow3lem2  19540  efgsfo  19651  lt6abl  19807  ghmcyg  19808  ablsimpgfind  20024  unitgrp  20277  irredrmul  20321  drngnidl  21093  znunit  21428  tgcl  22796  neiint  22932  restopnb  23003  ordtrest2lem  23031  pnfnei  23048  mnfnei  23049  iscnp4  23091  haust1  23180  ordthauslem  23211  tgcmp  23229  t1connperf  23264  2ndc1stc  23279  2ndcdisj  23284  islly2  23312  nllyrest  23314  reftr  23342  comppfsc  23360  ptbasfi  23409  ptcnp  23450  xkococnlem  23487  tgqtop  23540  fbssfi  23665  fgabs  23707  neifil  23708  trfil2  23715  elfm2  23776  elfm3  23778  rnelfmlem  23780  fmfnfmlem4  23785  flffbas  23823  fclsfnflim  23855  ptcmplem4  23883  tsmsxp  23983  blssexps  24256  blssex  24257  icccmplem3  24664  cnheibor  24805  pi1blem  24890  iscfil3  25125  iscmet3lem2  25144  metsscmetcld  25167  ovolicc2  25375  nulmbl2  25389  volsup  25409  dyadmbllem  25452  itg2const2  25595  bddmulibl  25692  bddiblnc  25695  limcflf  25734  itgsubst  25908  ulmdvlem3  26257  xrlimcnp  26819  amgm  26842  dchrptlem2  27117  lgsne0  27187  lgsqr  27203  lgsquadlem1  27232  dchrvmasumif  27355  rpvmasum2  27364  dchrisum0re  27365  dchrisum0lem3  27371  dchrisum0  27372  dchrmusum  27376  dchrvmasum  27377  chpdifbnd  27407  pntrlog2bnd  27436  pntibndlem3  27444  pntibnd  27445  pntleml  27463  ostth  27491  nosupno  27555  nosupbnd1lem1  27560  nosupbnd2  27568  noinfno  27570  noinfbnd1lem1  27575  noinfbnd2  27583  scutbdaybnd2  27668  oldlim  27732  oldbdayim  27734  sleadd1  27825  norecdiv  28009  precsexlem11  28034  noseqrdgfn  28098  brbtwn2  28635  colinearalg  28640  nbumgrvtx  29075  cusgrfilem1  29184  nmobndi  30500  spansneleq  31295  ofrn2  32337  xreceu  32558  ordtrest2NEWlem  33394  dya2iocnei  33773  connpconn  34717  cvmsss2  34756  cvmlift2lem10  34794  cvmlift3lem2  34802  outsidele  35600  neibastop1  35735  neibastop2lem  35736  matunitlindflem1  36978  mblfinlem1  37019  mblfinlem3  37021  mblfinlem4  37022  ismblfin  37023  cnambfre  37030  itg2addnclem  37033  itg2addnclem3  37035  ftc1anclem7  37061  ftc1anc  37063  fdc  37107  sstotbnd2  37136  sstotbnd  37137  isbndx  37144  ssbnd  37150  totbndbnd  37151  heibor  37183  unichnidl  37393  pexmidlem8N  39342  sn-0tie0  41826  nna4b4nsq  41916  elrfi  41946  fnwe2lem2  42307  hbtlem5  42384  rexlimdvaacbv  43471  rexlimddvcbvw  43472  liminfval2  44994  2zrngamgm  47133