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

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

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 3071

This theorem is referenced by:  rexlimddv  3161  tz7.7  6410  isofrlem  7360  nnawordex  8675  nnaordex2  8677  oaabs2  8687  fiin  9462  marypha1lem  9473  wemaplem3  9588  cantnflt  9712  fseqenlem2  10065  cardaleph  10129  coftr  10313  fin23lem26  10365  fin1a2lem13  10452  fpwwe2  10683  r1wunlim  10777  wunex2  10778  inttsk  10814  grur1  10860  inaprc  10876  receu  11908  zsupss  12979  xralrple  13247  rexanuz  15384  limsupval2  15516  caucvgb  15716  fsumiun  15857  rpnnen2lem12  16261  dvdsval2  16293  prmind2  16722  prmdvdsncoprmbd  16764  pcprmpw2  16920  pockthg  16944  prmreclem5  16958  vdwlem6  17024  vdwlem10  17028  sscpwex  17859  drsdirfi  18351  psgnunilem3  19514  sylow3lem2  19646  efgsfo  19757  lt6abl  19913  ghmcyg  19914  ablsimpgfind  20130  unitgrp  20383  irredrmul  20427  drngnidl  21253  znunit  21582  tgcl  22976  neiint  23112  restopnb  23183  ordtrest2lem  23211  pnfnei  23228  mnfnei  23229  iscnp4  23271  haust1  23360  ordthauslem  23391  tgcmp  23409  t1connperf  23444  2ndc1stc  23459  2ndcdisj  23464  islly2  23492  nllyrest  23494  reftr  23522  comppfsc  23540  ptbasfi  23589  ptcnp  23630  xkococnlem  23667  tgqtop  23720  fbssfi  23845  fgabs  23887  neifil  23888  trfil2  23895  elfm2  23956  elfm3  23958  rnelfmlem  23960  fmfnfmlem4  23965  flffbas  24003  fclsfnflim  24035  ptcmplem4  24063  tsmsxp  24163  blssexps  24436  blssex  24437  icccmplem3  24846  cnheibor  24987  pi1blem  25072  iscfil3  25307  iscmet3lem2  25326  metsscmetcld  25349  ovolicc2  25557  nulmbl2  25571  volsup  25591  dyadmbllem  25634  itg2const2  25776  bddmulibl  25874  bddiblnc  25877  limcflf  25916  itgsubst  26090  ulmdvlem3  26445  xrlimcnp  27011  amgm  27034  dchrptlem2  27309  lgsne0  27379  lgsqr  27395  lgsquadlem1  27424  dchrvmasumif  27547  rpvmasum2  27556  dchrisum0re  27557  dchrisum0lem3  27563  dchrisum0  27564  dchrmusum  27568  dchrvmasum  27569  chpdifbnd  27599  pntrlog2bnd  27628  pntibndlem3  27636  pntibnd  27637  pntleml  27655  ostth  27683  nosupno  27748  nosupbnd1lem1  27753  nosupbnd2  27761  noinfno  27763  noinfbnd1lem1  27768  noinfbnd2  27776  scutbdaybnd2  27861  oldlim  27925  oldbdayim  27927  sleadd1  28022  norecdiv  28216  precsexlem11  28241  noseqrdgfn  28312  brbtwn2  28920  colinearalg  28925  nbumgrvtx  29363  cusgrfilem1  29473  nmobndi  30794  spansneleq  31589  ofrn2  32650  xreceu  32904  ordtrest2NEWlem  33921  dya2iocnei  34284  connpconn  35240  cvmsss2  35279  cvmlift2lem10  35317  cvmlift3lem2  35325  outsidele  36133  neibastop1  36360  neibastop2lem  36361  matunitlindflem1  37623  mblfinlem1  37664  mblfinlem3  37666  mblfinlem4  37667  ismblfin  37668  cnambfre  37675  itg2addnclem  37678  itg2addnclem3  37680  ftc1anclem7  37706  ftc1anc  37708  fdc  37752  sstotbnd2  37781  sstotbnd  37782  isbndx  37789  ssbnd  37795  totbndbnd  37796  heibor  37828  unichnidl  38038  pexmidlem8N  39979  sn-0tie0  42469  nna4b4nsq  42670  elrfi  42705  fnwe2lem2  43063  hbtlem5  43140  rexlimdvaacbv  44218  rexlimddvcbvw  44219  relpfrlem  44974  liminfval2  45783  2zrngamgm  48161