Theorem rexlimdvaa 3209

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111  ∃wrex 3071

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 1911

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3075  df-rex 3076

This theorem is referenced by:  rexlimddv  3215  tz7.7  6200  isofrlem  7093  nnawordex  8279  oaabs2  8288  fiin  8932  marypha1lem  8943  wemaplem3  9058  cantnflt  9181  fseqenlem2  9498  cardaleph  9562  coftr  9746  fin23lem26  9798  fin1a2lem13  9885  fpwwe2  10116  r1wunlim  10210  wunex2  10211  inttsk  10247  grur1  10293  inaprc  10309  receu  11336  zsupss  12390  xralrple  12652  rexanuz  14766  limsupval2  14898  caucvgb  15097  fsumiun  15237  rpnnen2lem12  15639  dvdsval2  15671  prmind2  16094  prmdvdsncoprmbd  16135  pcprmpw2  16286  pockthg  16310  prmreclem5  16324  vdwlem6  16390  vdwlem10  16394  sscpwex  17157  drsdirfi  17627  psgnunilem3  18704  sylow3lem2  18833  efgsfo  18945  lt6abl  19096  ghmcyg  19097  ablsimpgfind  19313  unitgrp  19501  irredrmul  19541  drngnidl  20083  znunit  20344  tgcl  21682  neiint  21817  restopnb  21888  ordtrest2lem  21916  pnfnei  21933  mnfnei  21934  iscnp4  21976  haust1  22065  ordthauslem  22096  tgcmp  22114  t1connperf  22149  2ndc1stc  22164  2ndcdisj  22169  islly2  22197  nllyrest  22199  reftr  22227  comppfsc  22245  ptbasfi  22294  ptcnp  22335  xkococnlem  22372  tgqtop  22425  fbssfi  22550  fgabs  22592  neifil  22593  trfil2  22600  elfm2  22661  elfm3  22663  rnelfmlem  22665  fmfnfmlem4  22670  flffbas  22708  fclsfnflim  22740  ptcmplem4  22768  tsmsxp  22868  blssexps  23141  blssex  23142  icccmplem3  23538  cnheibor  23669  pi1blem  23753  iscfil3  23986  iscmet3lem2  24005  metsscmetcld  24028  ovolicc2  24235  nulmbl2  24249  volsup  24269  dyadmbllem  24312  itg2const2  24454  bddmulibl  24551  bddiblnc  24554  limcflf  24593  itgsubst  24761  ulmdvlem3  25109  xrlimcnp  25666  amgm  25688  dchrptlem2  25961  lgsne0  26031  lgsqr  26047  lgsquadlem1  26076  dchrvmasumif  26199  rpvmasum2  26208  dchrisum0re  26209  dchrisum0lem3  26215  dchrisum0  26216  dchrmusum  26220  dchrvmasum  26221  chpdifbnd  26251  pntrlog2bnd  26280  pntibndlem3  26288  pntibnd  26289  pntleml  26307  ostth  26335  brbtwn2  26811  colinearalg  26816  nbumgrvtx  27248  cusgrfilem1  27357  nmobndi  28670  spansneleq  29465  ofrn2  30512  xreceu  30732  ordtrest2NEWlem  31405  dya2iocnei  31780  connpconn  32725  cvmsss2  32764  cvmlift2lem10  32802  cvmlift3lem2  32810  nosupno  33503  nosupbnd1lem1  33508  nosupbnd2  33516  noinfno  33518  noinfbnd1lem1  33523  noinfbnd2  33531  scutbdaybnd2  33605  oldbdayim  33662  outsidele  34017  neibastop1  34131  neibastop2lem  34132  matunitlindflem1  35367  mblfinlem1  35408  mblfinlem3  35410  mblfinlem4  35411  ismblfin  35412  cnambfre  35419  itg2addnclem  35422  itg2addnclem3  35424  ftc1anclem7  35450  ftc1anc  35452  fdc  35497  sstotbnd2  35526  sstotbnd  35527  isbndx  35534  ssbnd  35540  totbndbnd  35541  heibor  35573  unichnidl  35783  pexmidlem8N  37587  sn-0tie0  39953  nna4b4nsq  40024  elrfi  40043  fnwe2lem2  40403  hbtlem5  40480  rexlimdvaacbv  41319  rexlimddvcbvw  41320  liminfval2  42811  2zrngamgm  44979