Theorem rexlimdvaa 3139

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∃wrex 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3062

This theorem is referenced by:  rexlimddv  3144  tz7.7  6349  isofrlem  7295  nnawordex  8573  nnaordex2  8575  oaabs2  8585  fiin  9335  marypha1lem  9346  wemaplem3  9463  cantnflt  9593  fseqenlem2  9947  cardaleph  10011  coftr  10195  fin23lem26  10247  fin1a2lem13  10334  fpwwe2  10566  r1wunlim  10660  wunex2  10661  inttsk  10697  grur1  10743  inaprc  10759  receu  11795  zsupss  12887  xralrple  13157  rexanuz  15308  limsupval2  15442  caucvgb  15642  fsumiun  15784  rpnnen2lem12  16192  dvdsval2  16224  prmind2  16654  prmdvdsncoprmbd  16697  pcprmpw2  16853  pockthg  16877  prmreclem5  16891  vdwlem6  16957  vdwlem10  16961  sscpwex  17782  drsdirfi  18271  psgnunilem3  19471  sylow3lem2  19603  efgsfo  19714  lt6abl  19870  ghmcyg  19871  ablsimpgfind  20087  unitgrp  20363  irredrmul  20407  drngnidl  21241  znunit  21543  tgcl  22934  neiint  23069  restopnb  23140  ordtrest2lem  23168  pnfnei  23185  mnfnei  23186  iscnp4  23228  haust1  23317  ordthauslem  23348  tgcmp  23366  t1connperf  23401  2ndc1stc  23416  2ndcdisj  23421  islly2  23449  nllyrest  23451  reftr  23479  comppfsc  23497  ptbasfi  23546  ptcnp  23587  xkococnlem  23624  tgqtop  23677  fbssfi  23802  fgabs  23844  neifil  23845  trfil2  23852  elfm2  23913  elfm3  23915  rnelfmlem  23917  fmfnfmlem4  23922  flffbas  23960  fclsfnflim  23992  ptcmplem4  24020  tsmsxp  24120  blssexps  24391  blssex  24392  icccmplem3  24790  cnheibor  24922  pi1blem  25006  iscfil3  25240  iscmet3lem2  25259  metsscmetcld  25282  ovolicc2  25489  nulmbl2  25503  volsup  25523  dyadmbllem  25566  itg2const2  25708  bddmulibl  25806  bddiblnc  25809  limcflf  25848  itgsubst  26016  ulmdvlem3  26367  xrlimcnp  26932  amgm  26954  dchrptlem2  27228  lgsne0  27298  lgsqr  27314  lgsquadlem1  27343  dchrvmasumif  27466  rpvmasum2  27475  dchrisum0re  27476  dchrisum0lem3  27482  dchrisum0  27483  dchrmusum  27487  dchrvmasum  27488  chpdifbnd  27518  pntrlog2bnd  27547  pntibndlem3  27555  pntibnd  27556  pntleml  27574  ostth  27602  nosupno  27667  nosupbnd1lem1  27672  nosupbnd2  27680  noinfno  27682  noinfbnd1lem1  27687  noinfbnd2  27695  cutbdaybnd2  27788  oldlim  27879  oldbdayim  27881  leadds1  27981  norecdiv  28182  precsexlem11  28209  noseqrdgfn  28298  pw2recs  28430  z12sge0  28475  brbtwn2  28974  colinearalg  28979  nbumgrvtx  29415  cusgrfilem1  29524  nmobndi  30846  spansneleq  31641  ofrn2  32713  xreceu  32981  ordtrest2NEWlem  34066  dya2iocnei  34426  connpconn  35417  cvmsss2  35456  cvmlift2lem10  35494  cvmlift3lem2  35502  outsidele  36314  neibastop1  36541  neibastop2lem  36542  ttctr  36675  dfttc2g  36688  dfttc4  36712  mh-inf3f1  36723  matunitlindflem1  37937  mblfinlem1  37978  mblfinlem3  37980  mblfinlem4  37981  ismblfin  37982  cnambfre  37989  itg2addnclem  37992  itg2addnclem3  37994  ftc1anclem7  38020  ftc1anc  38022  fdc  38066  sstotbnd2  38095  sstotbnd  38096  isbndx  38103  ssbnd  38109  totbndbnd  38110  heibor  38142  unichnidl  38352  pexmidlem8N  40423  sn-0tie0  42896  nna4b4nsq  43093  elrfi  43126  fnwe2lem2  43479  hbtlem5  43556  rexlimdvaacbv  44632  rexlimddvcbvw  44633  relpfrlem  45380  liminfval2  46196  2zrngamgm  48721