Theorem rexlimdvaa 3163

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141  ∃wrex 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-rex 3086

This theorem is referenced by:  rexlimddv  3168  tz7.7  6366  isofrlem  7318  nnawordex  8600  nnaordex2  8602  oaabs2  8612  fiin  9361  marypha1lem  9372  wemaplem3  9489  cantnflt  9620  fseqenlem2  9974  cardaleph  10038  coftr  10223  fin23lem26  10275  fin1a2lem13  10362  fpwwe2  10594  r1wunlim  10688  wunex2  10689  inttsk  10725  grur1  10771  inaprc  10787  receu  11825  zsupss  12931  xralrple  13201  rexanuz  15363  limsupval2  15497  caucvgb  15697  fsumiun  15839  rpnnen2lem12  16247  dvdsval2  16279  prmind2  16709  prmdvdsncoprmbd  16752  pcprmpw2  16908  pockthg  16932  prmreclem5  16946  vdwlem6  17012  vdwlem10  17016  sscpwex  17838  drsdirfi  18327  psgnunilem3  19526  sylow3lem2  19658  efgsfo  19769  lt6abl  19925  ghmcyg  19926  ablsimpgfind  20142  unitgrp  20418  irredrmul  20462  drngnidl  21300  znunit  21602  tgcl  23016  neiint  23151  restopnb  23222  ordtrest2lem  23250  pnfnei  23267  mnfnei  23268  iscnp4  23310  haust1  23399  ordthauslem  23430  tgcmp  23448  t1connperf  23483  2ndc1stc  23498  2ndcdisj  23503  islly2  23531  nllyrest  23533  reftr  23561  comppfsc  23579  ptbasfi  23628  ptcnp  23669  xkococnlem  23706  tgqtop  23759  fbssfi  23884  fgabs  23926  neifil  23927  trfil2  23934  elfm2  23995  elfm3  23997  rnelfmlem  23999  fmfnfmlem4  24004  flffbas  24042  fclsfnflim  24074  ptcmplem4  24102  tsmsxp  24202  blssexps  24473  blssex  24474  icccmplem3  24872  cnheibor  25004  pi1blem  25088  iscfil3  25322  iscmet3lem2  25341  metsscmetcld  25364  ovolicc2  25571  nulmbl2  25585  volsup  25605  dyadmbllem  25648  itg2const2  25790  bddmulibl  25888  bddiblnc  25891  limcflf  25930  itgsubst  26098  ulmdvlem3  26452  xrlimcnp  27020  amgm  27042  dchrptlem2  27316  lgsne0  27386  lgsqr  27402  lgsquadlem1  27431  dchrvmasumif  27554  rpvmasum2  27563  dchrisum0re  27564  dchrisum0lem3  27570  dchrisum0  27571  dchrmusum  27575  dchrvmasum  27576  chpdifbnd  27606  pntrlog2bnd  27635  pntibndlem3  27643  pntibnd  27644  pntleml  27662  ostth  27690  nosupno  27754  nosupbnd1lem1  27759  nosupbnd2  27767  noinfno  27769  noinfbnd1lem1  27774  noinfbnd2  27782  cutbdaybnd2  27876  oldlim  27967  oldbdayim  27969  leadds1  28069  norecdiv  28270  precsexlem11  28297  noseqrdgfn  28386  pw2recs  28518  z12sge0  28563  brbtwn2  29062  colinearalg  29067  nbumgrvtx  29503  cusgrfilem1  29612  nmobndi  30934  spansneleq  31729  ofrn2  32802  xreceu  33059  ordtrest2NEWlem  34179  dya2iocnei  34539  connpconn  35545  cvmsss2  35584  cvmlift2lem10  35622  cvmlift3lem2  35630  outsidele  36442  neibastop1  36679  neibastop2lem  36680  ttctr  36813  dfttc2g  36826  dfttc4  36850  mh-inf3f1  36861  matunitlindflem1  38075  mblfinlem1  38116  mblfinlem3  38118  mblfinlem4  38119  ismblfin  38120  cnambfre  38127  itg2addnclem  38130  itg2addnclem3  38132  ftc1anclem7  38158  ftc1anc  38160  fdc  38204  sstotbnd2  38233  sstotbnd  38234  isbndx  38241  ssbnd  38247  totbndbnd  38248  heibor  38280  unichnidl  38490  pexmidlem8N  40561  sn-0tie0  43033  nna4b4nsq  43202  elrfi  43235  fnwe2lem2  43588  hbtlem5  43665  rexlimdvaacbv  44741  rexlimddvcbvw  44742  relpfrlem  45489  liminfval2  46302  2zrngamgm  48827