Theorem rexlimdvaa 3285

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2110  ∃wrex 3139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-ral 3143  df-rex 3144

This theorem is referenced by:  rexlimddv  3291  tz7.7  6211  isofrlem  7087  nnawordex  8257  oaabs2  8266  fiin  8880  marypha1lem  8891  wemaplem3  9006  cantnflt  9129  fseqenlem2  9445  cardaleph  9509  coftr  9689  fin23lem26  9741  fin1a2lem13  9828  fpwwe2  10059  r1wunlim  10153  wunex2  10154  inttsk  10190  grur1  10236  inaprc  10252  receu  11279  zsupss  12331  xralrple  12592  rexanuz  14699  limsupval2  14831  caucvgb  15030  fsumiun  15170  rpnnen2lem12  15572  dvdsval2  15604  prmind2  16023  pcprmpw2  16212  pockthg  16236  prmreclem5  16250  vdwlem6  16316  vdwlem10  16320  sscpwex  17079  drsdirfi  17542  psgnunilem3  18618  sylow3lem2  18747  efgsfo  18859  lt6abl  19009  ghmcyg  19010  ablsimpgfind  19226  unitgrp  19411  irredrmul  19451  drngnidl  19996  znunit  20704  tgcl  21571  neiint  21706  restopnb  21777  ordtrest2lem  21805  pnfnei  21822  mnfnei  21823  iscnp4  21865  haust1  21954  ordthauslem  21985  tgcmp  22003  t1connperf  22038  2ndc1stc  22053  2ndcdisj  22058  islly2  22086  nllyrest  22088  reftr  22116  comppfsc  22134  ptbasfi  22183  ptcnp  22224  xkococnlem  22261  tgqtop  22314  fbssfi  22439  fgabs  22481  neifil  22482  trfil2  22489  elfm2  22550  elfm3  22552  rnelfmlem  22554  fmfnfmlem4  22559  flffbas  22597  fclsfnflim  22629  ptcmplem4  22657  tsmsxp  22757  blssexps  23030  blssex  23031  icccmplem3  23426  cnheibor  23553  pi1blem  23637  iscfil3  23870  iscmet3lem2  23889  metsscmetcld  23912  ovolicc2  24117  nulmbl2  24131  volsup  24151  dyadmbllem  24194  itg2const2  24336  bddmulibl  24433  limcflf  24473  itgsubst  24640  ulmdvlem3  24984  xrlimcnp  25540  amgm  25562  dchrptlem2  25835  lgsne0  25905  lgsqr  25921  lgsquadlem1  25950  dchrvmasumif  26073  rpvmasum2  26082  dchrisum0re  26083  dchrisum0lem3  26089  dchrisum0  26090  dchrmusum  26094  dchrvmasum  26095  chpdifbnd  26125  pntrlog2bnd  26154  pntibndlem3  26162  pntibnd  26163  pntleml  26181  ostth  26209  brbtwn2  26685  colinearalg  26690  nbumgrvtx  27122  cusgrfilem1  27231  nmobndi  28546  spansneleq  29341  ofrn2  30381  xreceu  30593  ordtrest2NEWlem  31160  dya2iocnei  31535  connpconn  32477  cvmsss2  32516  cvmlift2lem10  32554  cvmlift3lem2  32562  nosupno  33198  nosupbnd1lem1  33203  nosupbnd2  33211  scutbdaybnd  33270  outsidele  33588  neibastop1  33702  neibastop2lem  33703  matunitlindflem1  34882  mblfinlem1  34923  mblfinlem3  34925  mblfinlem4  34926  ismblfin  34927  cnambfre  34934  itg2addnclem  34937  itg2addnclem3  34939  bddiblnc  34956  ftc1anclem7  34967  ftc1anc  34969  fdc  35014  sstotbnd2  35046  sstotbnd  35047  isbndx  35054  ssbnd  35060  totbndbnd  35061  heibor  35093  unichnidl  35303  pexmidlem8N  37107  elrfi  39284  fnwe2lem2  39644  hbtlem5  39721  rexlimdvaacbv  40551  rexlimddvcbvw  40552  liminfval2  42042  2zrngamgm  44204