Theorem rexlimdvaa 3287

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114  ∃wrex 3141

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 209  df-an 399  df-ex 1781  df-ral 3145  df-rex 3146

This theorem is referenced by:  rexlimddv  3293  tz7.7  6219  isofrlem  7095  nnawordex  8265  oaabs2  8274  fiin  8888  marypha1lem  8899  wemaplem3  9014  cantnflt  9137  fseqenlem2  9453  cardaleph  9517  coftr  9697  fin23lem26  9749  fin1a2lem13  9836  fpwwe2  10067  r1wunlim  10161  wunex2  10162  inttsk  10198  grur1  10244  inaprc  10260  receu  11287  zsupss  12340  xralrple  12601  rexanuz  14707  limsupval2  14839  caucvgb  15038  fsumiun  15178  rpnnen2lem12  15580  dvdsval2  15612  prmind2  16031  pcprmpw2  16220  pockthg  16244  prmreclem5  16258  vdwlem6  16324  vdwlem10  16328  sscpwex  17087  drsdirfi  17550  psgnunilem3  18626  sylow3lem2  18755  efgsfo  18867  lt6abl  19017  ghmcyg  19018  ablsimpgfind  19234  unitgrp  19419  irredrmul  19459  drngnidl  20004  znunit  20712  tgcl  21579  neiint  21714  restopnb  21785  ordtrest2lem  21813  pnfnei  21830  mnfnei  21831  iscnp4  21873  haust1  21962  ordthauslem  21993  tgcmp  22011  t1connperf  22046  2ndc1stc  22061  2ndcdisj  22066  islly2  22094  nllyrest  22096  reftr  22124  comppfsc  22142  ptbasfi  22191  ptcnp  22232  xkococnlem  22269  tgqtop  22322  fbssfi  22447  fgabs  22489  neifil  22490  trfil2  22497  elfm2  22558  elfm3  22560  rnelfmlem  22562  fmfnfmlem4  22567  flffbas  22605  fclsfnflim  22637  ptcmplem4  22665  tsmsxp  22765  blssexps  23038  blssex  23039  icccmplem3  23434  cnheibor  23561  pi1blem  23645  iscfil3  23878  iscmet3lem2  23897  metsscmetcld  23920  ovolicc2  24125  nulmbl2  24139  volsup  24159  dyadmbllem  24202  itg2const2  24344  bddmulibl  24441  limcflf  24481  itgsubst  24648  ulmdvlem3  24992  xrlimcnp  25548  amgm  25570  dchrptlem2  25843  lgsne0  25913  lgsqr  25929  lgsquadlem1  25958  dchrvmasumif  26081  rpvmasum2  26090  dchrisum0re  26091  dchrisum0lem3  26097  dchrisum0  26098  dchrmusum  26102  dchrvmasum  26103  chpdifbnd  26133  pntrlog2bnd  26162  pntibndlem3  26170  pntibnd  26171  pntleml  26189  ostth  26217  brbtwn2  26693  colinearalg  26698  nbumgrvtx  27130  cusgrfilem1  27239  nmobndi  28554  spansneleq  29349  ofrn2  30389  xreceu  30600  ordtrest2NEWlem  31167  dya2iocnei  31542  connpconn  32484  cvmsss2  32523  cvmlift2lem10  32561  cvmlift3lem2  32569  nosupno  33205  nosupbnd1lem1  33210  nosupbnd2  33218  scutbdaybnd  33277  outsidele  33595  neibastop1  33709  neibastop2lem  33710  matunitlindflem1  34890  mblfinlem1  34931  mblfinlem3  34933  mblfinlem4  34934  ismblfin  34935  cnambfre  34942  itg2addnclem  34945  itg2addnclem3  34947  bddiblnc  34964  ftc1anclem7  34975  ftc1anc  34977  fdc  35022  sstotbnd2  35054  sstotbnd  35055  isbndx  35062  ssbnd  35068  totbndbnd  35069  heibor  35101  unichnidl  35311  pexmidlem8N  37115  elrfi  39298  fnwe2lem2  39658  hbtlem5  39735  rexlimdvaacbv  40565  rexlimddvcbvw  40566  liminfval2  42056  2zrngamgm  44217