Theorem rexlimdvaa 3173

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-rex 3096

This theorem is referenced by:  rexlimddv  3178  tz7.7  6383  isofrlem  7336  nnawordex  8619  nnaordex2  8621  oaabs2  8631  fiin  9378  marypha1lem  9389  wemaplem3  9506  cantnflt  9637  fseqenlem2  10005  cardaleph  10069  coftr  10253  fin23lem26  10305  fin1a2lem13  10392  fpwwe2  10624  r1wunlim  10718  wunex2  10719  inttsk  10755  grur1  10801  inaprc  10817  receu  11855  zsupss  12957  xralrple  13227  rexanuz  15393  limsupval2  15527  caucvgb  15727  fsumiun  15869  rpnnen2lem12  16277  dvdsval2  16309  prmind2  16739  prmdvdsncoprmbd  16782  pcprmpw2  16938  pockthg  16962  prmreclem5  16976  vdwlem6  17042  vdwlem10  17046  sscpwex  17868  drsdirfi  18357  psgnunilem3  19562  sylow3lem2  19694  efgsfo  19805  lt6abl  19961  ghmcyg  19962  ablsimpgfind  20178  unitgrp  20461  irredrmul  20505  unichnlidl  21336  drngnidl  21347  znunit  21678  tgcl  23091  neiint  23226  restopnb  23297  ordtrest2lem  23325  pnfnei  23342  mnfnei  23343  iscnp4  23385  haust1  23474  ordthauslem  23505  tgcmp  23523  t1connperf  23558  2ndc1stc  23573  2ndcdisj  23578  islly2  23606  nllyrest  23608  reftr  23636  comppfsc  23654  ptbasfi  23703  ptcnp  23744  xkococnlem  23781  tgqtop  23834  fbssfi  23959  fgabs  24001  neifil  24002  trfil2  24009  elfm2  24070  elfm3  24072  rnelfmlem  24074  fmfnfmlem4  24079  flffbas  24117  fclsfnflim  24149  ptcmplem4  24177  tsmsxp  24277  blssexps  24548  blssex  24549  icccmplem3  24947  cnheibor  25079  pi1blem  25163  iscfil3  25397  iscmet3lem2  25416  metsscmetcld  25439  ovolicc2  25646  nulmbl2  25660  volsup  25680  dyadmbllem  25723  itg2const2  25865  bddmulibl  25963  bddiblnc  25966  limcflf  26005  itgsubst  26173  ulmdvlem3  26527  xrlimcnp  27095  amgm  27117  dchrptlem2  27391  lgsne0  27461  lgsqr  27477  lgsquadlem1  27506  dchrvmasumif  27629  rpvmasum2  27638  dchrisum0re  27639  dchrisum0lem3  27645  dchrisum0  27646  dchrmusum  27650  dchrvmasum  27651  chpdifbnd  27681  pntrlog2bnd  27710  pntibndlem3  27718  pntibnd  27719  pntleml  27737  ostth  27765  nosupno  27829  nosupbnd1lem1  27834  nosupbnd2  27842  noinfno  27844  noinfbnd1lem1  27849  noinfbnd2  27857  cutbdaybnd2  27951  oldlim  28042  oldbdayim  28044  leadds1  28144  norecdiv  28345  precsexlem11  28372  noseqrdgfn  28461  pw2recs  28593  z12sge0  28638  brbtwn2  29192  colinearalg  29197  nbumgrvtx  29633  cusgrfilem1  29742  nmobndi  31064  spansneleq  31859  ofrn2  32922  xreceu  33178  ordtrest2NEWlem  34253  dya2iocnei  34613  connpconn  35622  cvmsss2  35661  cvmlift2lem10  35699  cvmlift3lem2  35707  outsidele  36519  neibastop1  36755  neibastop2lem  36756  ttctr  36889  dfttc2g  36902  dfttc4  36926  mh-inf3f1  36937  matunitlindflem1  38150  mblfinlem1  38191  mblfinlem3  38193  mblfinlem4  38194  ismblfin  38195  cnambfre  38202  itg2addnclem  38205  itg2addnclem3  38207  ftc1anclem7  38233  ftc1anc  38235  fdc  38279  sstotbnd2  38308  sstotbnd  38309  isbndx  38316  ssbnd  38322  totbndbnd  38323  heibor  38355  unichnidl  38565  pexmidlem8N  40636  sn-0tie0  43108  nna4b4nsq  43277  elrfi  43310  fnwe2lem2  43663  hbtlem5  43740  rexlimdvaacbv  44814  rexlimddvcbvw  44815  relpfrlem  45547  liminfval2  46367  2zrngamgm  48892